nothing to prove
Definition
A contraction sequence of a finite simple graph is a sequence of vertex partitions: it starts at the partition into singletons and merges two parts at every step, until at most one part remains. Two parts are homogeneous if has either all possible edges between them or none; the red degree of a part is the number of other parts it is not homogeneous with. The width of a contraction sequence is the largest red degree of any part occurring in it.
The twin-width is the least such that has a contraction sequence of width at most .
Lean source
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | import Mathlib.Data.Set.Card |
| 3 | import Mathlib.Data.Nat.Lattice |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Twin-width |
| 8 | type: definition |
| 9 | --- |
| 10 | A contraction sequence of a finite simple graph $G$ is a sequence of vertex |
| 11 | partitions: it starts at the partition into singletons and merges two parts |
| 12 | at every step, until at most one part remains. Two parts are homogeneous if |
| 13 | $G$ has either all possible edges between them or none; the red degree of a |
| 14 | part is the number of other parts it is not homogeneous with. The width of a |
| 15 | contraction sequence is the largest red degree of any part occurring in it. |
| 16 | |
| 17 | The twin-width $\operatorname{tww}(G)$ is the least $d$ such that $G$ has a |
| 18 | contraction sequence of width at most $d$. |
| 19 | |
| 20 | # Formalization notes |
| 21 | |
| 22 | Contracting in any order gives a sequence of width at most $|V(G)|$, so the |
| 23 | infimum in `twinWidth` ranges over a nonempty set. Because every state is |
| 24 | reached from the singleton partition by merges, each `partition i` with |
| 25 | `i ≤ stepCount` is automatically a partition of the vertex set; values of |
| 26 | `partition` beyond `stepCount` are irrelevant. |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax1.TwinWidth |
| 30 | |
| 31 | /-- Two vertex sets are homogeneous in `G`: either every pair of vertices |
| 32 | across them is adjacent, or none is. -/ |
| 33 | def Homogeneous {V : Type} (G : SimpleGraph V) (A B : Finset V) : Prop := |
| 34 | (∀ a ∈ A, ∀ b ∈ B, G.Adj a b) ∨ (∀ a ∈ A, ∀ b ∈ B, ¬ G.Adj a b) |
| 35 | |
| 36 | /-- The red degree of a part `A` in a family of parts `P`: the number of |
| 37 | other parts of `P` that are not homogeneous with `A`. -/ |
| 38 | noncomputable def redDegree {V : Type} (G : SimpleGraph V) |
| 39 | (P : Finset (Finset V)) (A : Finset V) : ℕ := |
| 40 | {B | B ∈ P ∧ B ≠ A ∧ ¬ Homogeneous G A B}.ncard |
| 41 | |
| 42 | /-- The partition of a finite vertex type into singletons. -/ |
| 43 | def singletonPartition (V : Type) [Fintype V] [DecidableEq V] : |
| 44 | Finset (Finset V) := |
| 45 | Finset.univ.image fun v : V => ({v} : Finset V) |
| 46 | |
| 47 | /-- A contraction sequence for `G` of width at most `d`: starting from the |
| 48 | singleton partition, each step merges two parts, until at most one part |
| 49 | remains; every part of every partition in the sequence has red degree at |
| 50 | most `d`. -/ |
| 51 | structure ContractionSequence {V : Type} [Fintype V] [DecidableEq V] |
| 52 | (G : SimpleGraph V) (d : ℕ) where |
| 53 | /-- The number of merge steps. -/ |
| 54 | stepCount : ℕ |
| 55 | /-- The state after each number of merge steps. -/ |
| 56 | partition : ℕ → Finset (Finset V) |
| 57 | /-- The sequence starts at the singleton partition. -/ |
| 58 | starts : partition 0 = singletonPartition V |
| 59 | /-- The sequence ends with at most one part. -/ |
| 60 | ends : (partition stepCount).card ≤ 1 |
| 61 | /-- Each step merges two distinct parts and keeps all other parts. -/ |
| 62 | step_merges : |
| 63 | ∀ i, i < stepCount → ∃ A ∈ partition i, ∃ B ∈ partition i, A ≠ B ∧ |
| 64 | partition (i + 1) = insert (A ∪ B) (((partition i).erase A).erase B) |
| 65 | /-- Every part of every partition in the sequence has red degree at most |
| 66 | `d`. -/ |
| 67 | redDegree_le : |
| 68 | ∀ i, i ≤ stepCount → ∀ ⦃A⦄, A ∈ partition i → |
| 69 | redDegree G (partition i) A ≤ d |
| 70 | |
| 71 | /-- `G` admits a contraction sequence of width at most `d`. -/ |
| 72 | def HasTwinWidthAtMost {V : Type} [Fintype V] [DecidableEq V] |
| 73 | (G : SimpleGraph V) (d : ℕ) : Prop := |
| 74 | Nonempty (ContractionSequence G d) |
| 75 | |
| 76 | /-- The twin-width of a finite simple graph: the least `d` such that the |
| 77 | graph has a contraction sequence of width at most `d`. -/ |
| 78 | noncomputable def twinWidth {V : Type} [Fintype V] [DecidableEq V] |
| 79 | (G : SimpleGraph V) : ℕ := |
| 80 | sInf {d | HasTwinWidthAtMost G d} |
| 81 | |
| 82 | end Lax1.TwinWidth |
| 83 |
Formalization notes
Contracting in any order gives a sequence of width at most , so the
infimum in twinWidth ranges over a nonempty set. Because every state is
reached from the singleton partition by merges, each partition i with
i ≤ stepCount is automatically a partition of the vertex set; values of
partition beyond stepCount are irrelevant.
Imported
none