Lax48.TwinWidth

Twin-width

concepts/Lax48/TwinWidth.lean · lax-48

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 1 of this submission's paper
page 4 of this submission's paper
page 2 of the paper of lax-242665, An Introduction to Lax

Definition

A partition sequence of a finite simple graph G is a sequence of partitions of its vertex set that starts at the partition into singletons, merges two parts into one at every step, and ends at the partition with a single part. Two parts of a same partition are homogeneous if either every pair of vertices across them is adjacent or none is; two non-homogeneous parts are red-adjacent. The red degree of a part is the number of other parts of its partition that are red-adjacent to it.

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

Formalization notes

The partitions are indexed by the number of merges performed so far, and values of $partition$ beyond $stepCount$ are irrelevant. 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. Merging in any order gives a partition sequence whose red degrees are at most the number of vertices, so the infimum in $twinWidth$ ranges over a nonempty set.

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive