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