Paper
Graph Classes and Width Parameters
5 pages · 47 marked passages · pdflatex · download PDF · lax-326031
-
Graph classes
A graph class is a set of finite simple graphs. A class contains, for each number of vertices n, some of the simple graphs on the canonical n-element vertex type.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 … module docstring, 19 lines 22 23 namespace Lax199508.GraphClasses 24 25 /-- A class of finite simple graphs: for each number of vertices `n`, a 26 predicate on the simple graphs over the canonical `n`-element type. -/ 27 abbrev GraphClass : Type := ∀ n : ℕ, SimpleGraph (Fin n) → Prop 28 29 end Lax199508.GraphClasses 30 -
Graph classes
A graph class is a class of finite simple graphs which is closed under isomorphism: if and , then .
Graph classes are ordered by inclusion, , written . The intersection and the union of a family of graph classes are again graph classes, written and .
1 import Mathlib.Combinatorics.SimpleGraph.Maps 2 import Mathlib.Order.SetNotation 3 … module docstring, 30 lines 34 35 namespace Lax871432.GraphClasses 36 37 /-- A class of finite simple graphs, given by an isomorphism-invariant predicate on the 38 finite simple graphs. -/ 39 structure GraphClass where 40 /-- The graphs of the class. -/ 41 Mem : ∀ {V : Type} [Finite V], SimpleGraph V → Prop 42 /-- The class is invariant under isomorphism. -/ 43 mem_congr : ∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} {F' : SimpleGraph W}, 44 Nonempty (F ≃g F') → (Mem F ↔ Mem F') 45 46 /-- Inclusion of graph classes: `𝓕 ≤ 𝓕'` if every graph in `𝓕` is in `𝓕'`. -/ 47 instance : PartialOrder GraphClass where 48 le 𝓕 𝓕' := ∀ ⦃V : Type⦄ [Finite V] (F : SimpleGraph V), 𝓕.Mem F → 𝓕'.Mem F 49 le_refl _ _ _ _ hF := hF 50 le_trans _ _ _ h h' _ _ F hF := h' F (h F hF) 51 le_antisymm := by 52 rintro ⟨Mem, _⟩ ⟨Mem', _⟩ h h' 53 have : @Mem = @Mem' := by 54 funext V _ F 55 exact propext ⟨h F, h' F⟩ 56 subst this 57 rfl 58 59 /-- The intersection of a set of graph classes: the graphs lying in each of them. The 60 intersection of a family is written `⨅ i, 𝓕 i`. -/ 61 instance : InfSet GraphClass where 62 sInf S := 63 { Mem F := ∀ 𝓕 ∈ S, 𝓕.Mem F 64 mem_congr he := 65 forall_congr' fun 𝓕 : GraphClass => imp_congr_right fun _ => 𝓕.mem_congr he } 66 67 /-- The union of a set of graph classes: the graphs lying in at least one of them. The union 68 of a family is written `⨆ i, 𝓕 i`. -/ 69 instance : SupSet GraphClass where 70 sSup S := 71 { Mem F := ∃ 𝓕 ∈ S, 𝓕.Mem F 72 mem_congr he := exists_congr fun 𝓕 : GraphClass => and_congr_right' (𝓕.mem_congr he) } 73 74 end Lax871432.GraphClasses 75 -
Closure properties of graph classes
Five closure properties of a class of finite simple graphs.
is closed under taking summands if implies and , where denotes disjoint union, and union-closed if conversely implies . It is minor-closed if every minor of a member is a member.
It is closed under taking induced subgraphs if every induced subgraph of a member is a member, and closed under contracting edges if every graph obtained from a member by contracting edges is a member.
1 import Mathlib.Combinatorics.SimpleGraph.Sum 2 import Mathlib.Data.Finite.Sum 3 import Lax68.GraphMinors 4 import Lax871432.Contractions 5 import Lax871432.GraphClasses 6 … module docstring, 17 lines 24 25 open Lax871432.Contractions Lax871432.GraphClasses 26 27 namespace Lax871432.ClosureProperties 28 29 /-- `𝓕` is *closed under taking summands* if both summands of a disjoint union in the class 30 are themselves in the class. -/ 31 def IsSummandClosed (𝓕 : GraphClass) : Prop := 32 ∀ {V W : Type} [Finite V] [Finite W] (F₁ : SimpleGraph V) (F₂ : SimpleGraph W), 33 𝓕.Mem (F₁ ⊕g F₂) → 𝓕.Mem F₁ ∧ 𝓕.Mem F₂ 34 35 /-- `𝓕` is *union-closed* if the disjoint union of two members is a member. -/ 36 def IsUnionClosed (𝓕 : GraphClass) : Prop := 37 ∀ {V W : Type} [Finite V] [Finite W] (F₁ : SimpleGraph V) (F₂ : SimpleGraph W), 38 𝓕.Mem F₁ → 𝓕.Mem F₂ → 𝓕.Mem (F₁ ⊕g F₂) 39 40 /-- `𝓕` is *closed under taking induced subgraphs* if every induced subgraph of a member is a 41 member. -/ 42 def IsInducedSubgraphClosed (𝓕 : GraphClass) : Prop := 43 ∀ {V : Type} [Finite V] (F : SimpleGraph V) (U : Set V), 𝓕.Mem F → 𝓕.Mem (F.induce U) 44 45 /-- `𝓕` is *closed under contracting edges* if every quotient of a member by a partition into 46 connected parts is a member. -/ 47 def IsContractionClosed (𝓕 : GraphClass) : Prop := 48 ∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} (K : SimpleGraph W), 49 IsContraction K F → 𝓕.Mem F → 𝓕.Mem K 50 51 /-- `𝓕` is *minor-closed* if every minor of a member is a member. -/ 52 def IsMinorClosed (𝓕 : GraphClass) : Prop := 53 ∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} (K : SimpleGraph W), 54 Lax68.GraphMinors.IsMinor K F → 𝓕.Mem F → 𝓕.Mem K 55 56 end Lax871432.ClosureProperties 57 -
Graph parameters and functional equivalence
A graph parameter assigns a natural number to every finite simple graph. Two graph parameters p and q are functionally equivalent when each is bounded by a numerical function of the other: there are functions f, g : ℕ → ℕ such that every finite simple graph G satisfies both p(G) ≤ f(q(G)) and q(G) ≤ g(p(G)). Functionally equivalent parameters are bounded on exactly the same classes of graphs.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 … module docstring, 24 lines 27 28 namespace Lax153141.GraphParameters 29 30 /-- A natural-valued parameter of finite simple graphs, in the uniform 31 signature shared by all graph parameters in this archive. -/ 32 abbrev GraphParam := 33 ∀ {V : Type} [Fintype V] [DecidableEq V], SimpleGraph V → ℕ 34 35 /-- Each of two graph parameters is bounded by a numerical function of the 36 other. -/ 37 def FunctionallyEquivalent (p q : GraphParam) : Prop := 38 (∃ f : ℕ → ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V] 39 (G : SimpleGraph V), p G ≤ f (q G)) ∧ 40 (∃ g : ℕ → ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V] 41 (G : SimpleGraph V), q G ≤ g (p G)) 42 43 end Lax153141.GraphParameters 44 -
def
Lax68.PathsPaths
Path graph illustration A finite path graph is a graph isomorphic to the standard path graph on a positive number of vertices.
1 import Mathlib.Combinatorics.SimpleGraph.Hasse 2 … module docstring, 11 lines 14 15 set_option autoImplicit false 16 17 namespace Lax68.Paths 18 19 def HasPathShape {V : Type*} (G : SimpleGraph V) : Prop := 20 ∃ n : ℕ, 21 0 < n ∧ 22 Nonempty (G ≃g SimpleGraph.pathGraph n) 23 24 def IsPath {V : Type*} (G : SimpleGraph V) : Prop := 25 HasPathShape G 26 27 end Lax68.Paths 28 -
def
Lax68.StarsStars
Star graph illustration A star has a centre adjacent to every other vertex and has no edges between two non-central vertices.
1 import Mathlib.Combinatorics.SimpleGraph.UniversalVerts 2 … module docstring, 11 lines 14 15 set_option autoImplicit false 16 17 namespace Lax68.Stars 18 19 def HasStarShape {V : Type*} (G : SimpleGraph V) : Prop := 20 ∃ centre : V, 21 centre ∈ G.universalVerts ∧ 22 ∀ ⦃u v⦄, G.Adj u v → u = centre ∨ v = centre 23 24 def IsStar {V : Type*} (G : SimpleGraph V) : Prop := 25 HasStarShape G 26 27 end Lax68.Stars 28 -
def
Lax68.TreesTrees
Tree illustration A tree is a connected acyclic simple graph, using mathlib's native predicate.
1 import Mathlib.Combinatorics.SimpleGraph.Acyclic 2 … module docstring, 11 lines 14 15 set_option autoImplicit false 16 17 namespace Lax68.Trees 18 19 def IsTree {V : Type*} (G : SimpleGraph V) : Prop := 20 G.IsTree 21 22 end Lax68.Trees 23 -
Ladders
Ladder graph illustration A finite ladder is a nonempty two-row grid: two paths joined by corresponding rungs.
1 import Mathlib.Combinatorics.SimpleGraph.Hasse 2 … module docstring, 11 lines 14 15 set_option autoImplicit false 16 17 namespace Lax68.Ladders 18 19 def HasLadderShape {V : Type*} (G : SimpleGraph V) : Prop := 20 ∃ n : ℕ, 21 0 < n ∧ 22 Nonempty 23 (G ≃g (SimpleGraph.pathGraph n □ SimpleGraph.pathGraph 2)) 24 25 def IsLadder {V : Type*} (G : SimpleGraph V) : Prop := 26 HasLadderShape G 27 28 end Lax68.Ladders 29 -
Triangles
Triangle graph illustration A triangle is a finite complete graph on exactly three vertices.
1 import Mathlib.Combinatorics.SimpleGraph.Maps 2 … module docstring, 10 lines 13 14 set_option autoImplicit false 15 16 namespace Lax68.Triangles 17 18 def IsTriangle {V : Type*} (G : SimpleGraph V) : Prop := 19 Nonempty (G ≃g SimpleGraph.completeGraph (Fin 3)) 20 21 end Lax68.Triangles 22 -
Maximal outerplanar graphs
Maximal outerplanar illustration An outerplanar graph is maximal outerplanar when no edge can be added between its existing vertices while preserving outerplanarity.
1 import Lax68.Outerplanar 2 … module docstring, 11 lines 14 15 set_option autoImplicit false 16 17 namespace Lax68.MaximalOuterplanar 18 19 def IsMaximalOuterplanar {V : Type*} 20 (G : SimpleGraph V) : Prop := 21 Outerplanar.IsOuterplanar G ∧ 22 ∀ H : SimpleGraph V, 23 G < H → 24 ¬ Outerplanar.IsOuterplanar H 25 26 end Lax68.MaximalOuterplanar 27 -
Outerplanar graphs
Outerplanar graph illustration A graph is outerplanar here when it has a crossing-free straight-line drawing with every vertex on one circle, a compact certificate for having every vertex on the boundary of the outer face.
1 import Lax68.GraphMinors 2 import Lax68.StraightLineDrawings 3 … module docstring, 12 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.Outerplanar 20 21 structure OuterplaneDrawing {V : Type*} (G : SimpleGraph V) 22 extends StraightLineDrawings.StraightLineDrawing G where 23 radius : ℝ 24 radius_pos : 0 < radius 25 onBoundary : 26 ∀ v : V, 27 let p := toStraightLineDrawing.point v 28 p.1 ^ 2 + p.2 ^ 2 = radius ^ 2 29 30 def IsOuterplanar {V : Type*} (G : SimpleGraph V) : Prop := 31 Nonempty (OuterplaneDrawing G) 32 33 /-- The usual forbidden-minor characterization of outerplanarity. -/ 34 def IsOuterplanarByExcludedMinors {V : Type*} (G : SimpleGraph V) : Prop := 35 ¬ GraphMinors.IsMinor GraphMinors.K4 G ∧ 36 ¬ GraphMinors.IsMinor GraphMinors.K23 G 37 38 end Lax68.Outerplanar 39 -
Series-parallel graphs
Series-parallel graph illustration A finite two-terminal series-parallel graph is built from a single terminal edge by series and parallel composition. The side conditions say that the composed graphs meet only at the intended terminals, and the final support condition excludes unused isolated vertices.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 … module docstring, 13 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.SeriesParallel 20 21 def edgeGraph {V : Type*} (s t : V) : SimpleGraph V := 22 SimpleGraph.fromRel fun u v => 23 (u = s ∧ v = t) ∨ 24 (u = t ∧ v = s) 25 26 inductive TwoTerminal {V : Type*} : SimpleGraph V → V → V → Prop 27 | edge (s t : V) (hne : s ≠ t) : 28 TwoTerminal (edgeGraph s t) s t 29 | series 30 {G H : SimpleGraph V} 31 {s m t : V} 32 (left : TwoTerminal G s m) 33 (right : TwoTerminal H m t) 34 (meet : 35 ∀ v, 36 v ∈ G.support → 37 v ∈ H.support → 38 v = m) : 39 TwoTerminal (G ⊔ H) s t 40 | parallel 41 {G H : SimpleGraph V} 42 {s t : V} 43 (left : TwoTerminal G s t) 44 (right : TwoTerminal H s t) 45 (meet : 46 ∀ v, 47 v ∈ G.support → 48 v ∈ H.support → 49 v = s ∨ v = t) : 50 TwoTerminal (G ⊔ H) s t 51 52 def IsSeriesParallel {V : Type*} (G : SimpleGraph V) : Prop := 53 ∃ s t, 54 TwoTerminal G s t ∧ 55 G.support = Set.univ 56 57 end Lax68.SeriesParallel 58 -
Triangulations
Triangulation illustration A triangulation of a graph G is a planar supergraph T on the same vertex set, with at least three vertices, to which no edge can be added while preserving planarity. For a plane embedding this is equivalent to every face of T being bounded by a triangle.
1 import Lax68.Planar 2 … module docstring, 13 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.Triangulations 20 21 def IsTriangulationOf {V : Type*} 22 (G T : SimpleGraph V) : Prop := 23 (∃ a b c : V, a ≠ b ∧ a ≠ c ∧ b ≠ c) ∧ 24 G ≤ T ∧ 25 Planar.IsPlanar T ∧ 26 ∀ H : SimpleGraph V, 27 T < H → 28 ¬ Planar.IsPlanar H 29 30 end Lax68.Triangulations 31 -
Grids and walls
Grid and wall illustration A nonempty rectangular grid has vertices in rows and columns, with edges between orthogonally consecutive positions. A wall is the brick-wall subgraph obtained by retaining alternating vertical grid edges.
1 import Mathlib.Combinatorics.SimpleGraph.Hasse 2 … module docstring, 12 lines 15 16 set_option autoImplicit false 17 18 namespace Lax68.GridsAndWalls 19 20 def consecutive (a b : ℕ) : Prop := 21 a + 1 = b ∨ b + 1 = a 22 23 def WallAdjacent {m n : ℕ} (u v : Fin m × Fin n) : Prop := 24 (u.1 = v.1 ∧ consecutive u.2.val v.2.val) ∨ 25 (u.2 = v.2 ∧ 26 consecutive u.1.val v.1.val ∧ 27 (Nat.min u.1.val v.1.val + u.2.val) % 2 = 0) 28 29 def HasGridShape {V : Type*} (G : SimpleGraph V) : Prop := 30 ∃ m n : ℕ, 31 0 < m ∧ 32 0 < n ∧ 33 Nonempty 34 (G ≃g (SimpleGraph.pathGraph m □ SimpleGraph.pathGraph n)) 35 36 def HasWallShape {V : Type*} (G : SimpleGraph V) : Prop := 37 ∃ m n : ℕ, 38 0 < m ∧ 39 0 < n ∧ 40 ∃ e : Fin m × Fin n ≃ V, 41 ∀ u v, 42 G.Adj (e u) (e v) ↔ WallAdjacent u v 43 44 def IsGrid {V : Type*} (G : SimpleGraph V) : Prop := 45 HasGridShape G 46 47 def IsWall {V : Type*} (G : SimpleGraph V) : Prop := 48 HasWallShape G 49 50 end Lax68.GridsAndWalls 51 -
def
Lax68.PlanarPlanar graphs
Planar graph illustration A graph is planar here when it has a crossing-free straight-line drawing in the real plane. For finite simple graphs, this agrees with the usual notion of planarity. The drawing certificate is supplied by a separate concept.
1 import Lax68.GraphMinors 2 import Lax68.StraightLineDrawings 3 … module docstring, 12 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.Planar 20 21 /-- Existence of a crossing-free straight-line drawing in the real plane. -/ 22 def IsPlanar {V : Type*} (G : SimpleGraph V) : Prop := 23 StraightLineDrawings.HasStraightLineDrawing G 24 25 def IsPlanarByExcludedMinors {V : Type*} (G : SimpleGraph V) : Prop := 26 ¬GraphMinors.IsMinor GraphMinors.K5 G ∧ 27 ¬GraphMinors.IsMinor GraphMinors.K33 G 28 29 end Lax68.Planar 30 -
χ-Boundedness
A class of finite simple graphs is χ-bounded if the chromatic number of each graph in the class is bounded by a function of its clique number.
1 import Lax9.MergeWidth 2 … module docstring, 8 lines 11 12 namespace Lax9.ChiBoundedness 13 14 open Lax9.MergeWidth 15 16 /-- A graph class is χ-bounded if there is a function such that every 17 is -colourable. -/ 18 def ChiBounded (C : GraphClass) : Prop := 19 ∃ f : ℕ → ℕ, ∀ ⦃V : Type⦄ [Fintype V] (G : SimpleGraph V), C G → 20 G.Colorable (f G.cliqueNum) 21 22 end Lax9.ChiBoundedness 23 -
Feedback vertex number
Let be a finite undirected simple graph. A feedback vertex set is a set for which the induced graph is acyclic. The feedback vertex number is
The minimum exists because deleting all vertices leaves an acyclic graph.
1 import Mathlib.Combinatorics.SimpleGraph.Acyclic 2 import Mathlib.Data.Nat.Lattice 3 import Mathlib.Data.Set.Card 4 … module docstring, 14 lines 19 20 namespace Lax379983.FeedbackVertexNumber 21 22 /-- The minimum number of vertices whose deletion makes the graph acyclic. -/ 23 noncomputable def feedbackVertexNumber {V : Type*} [Finite V] (G : SimpleGraph V) : ℕ := 24 sInf {n : ℕ | ∃ S : Set V, S.ncard = n ∧ (G.induce Sᶜ).IsAcyclic} 25 26 end Lax379983.FeedbackVertexNumber 27 -
Feedback edge number
Let be a finite undirected simple graph. A feedback edge set is a set for which the graph , obtained by deleting the edges in and retaining all vertices, is acyclic. The feedback edge number is
The minimum exists because deleting all edges leaves an acyclic graph.
1 import Mathlib.Combinatorics.SimpleGraph.Acyclic 2 import Mathlib.Data.Nat.Lattice 3 import Mathlib.Data.Set.Card 4 … module docstring, 14 lines 19 20 namespace Lax379983.FeedbackEdgeNumber 21 22 /-- The minimum number of edges whose deletion makes the graph acyclic. -/ 23 noncomputable def feedbackEdgeNumber {V : Type*} [Finite V] (G : SimpleGraph V) : ℕ := 24 sInf {n : ℕ | ∃ F : Set (Sym2 V), 25 F ⊆ G.edgeSet ∧ F.ncard = n ∧ (G.deleteEdges F).IsAcyclic} 26 27 end Lax379983.FeedbackEdgeNumber 28 -
Admissibility
Fix a linear ordering of the vertices of a graph G. An admissible family of size k at a vertex v consists of k paths of length at most r that start at v, end at vertices smaller than v, and are pairwise disjoint apart from v. The r-admissibility adm_r(G) is the minimum over all orderings of the largest k + 1 for which some vertex of G carries an admissible family of size k. Counting v itself is the usual convention: it makes admissibility at least 1 and at most the strong r-coloring number.
This is Definition 2.2 of Chapter 2 of the source lecture notes (2019/20 edition), minimized over vertex orderings as in their Definition 2.3; the notes give the same rationale for the +1, namely consistency with the reachability sets, which contain the vertex itself.
1 import Lax199508.GraphClasses 2 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic 3 import Mathlib.Data.Nat.Lattice 4 … module docstring, 38 lines 43 44 namespace Lax199508.Admissibility 45 46 open Lax199508.GraphClasses 47 48 /-- An admissible family of `k` paths at `v` under the ordering `π`: 49 `k` walks of length at most `r` out of `v`, each ending strictly before 50 `v` in the ordering, pairwise meeting only in `v`. -/ 51 structure AdmFamily {n : ℕ} (G : SimpleGraph (Fin n)) 52 (π : Equiv.Perm (Fin n)) (r k : ℕ) (v : Fin n) where 53 /-- The endpoint of each path. -/ 54 target : Fin k → Fin n 55 /-- The path from `v` to each endpoint. -/ 56 path : ∀ i, G.Walk v (target i) 57 /-- Every endpoint comes strictly before `v` in the ordering. -/ 58 target_lt : ∀ i, π (target i) < π v 59 /-- Every path has length at most `r`. -/ 60 length_le : ∀ i, (path i).length ≤ r 61 /-- Distinct paths meet only in `v`. -/ 62 meet_eq : ∀ i j, i ≠ j → ∀ y ∈ (path i).support, 63 y ∈ (path j).support → y = v 64 65 /-- Some vertex ordering admits no admissible family of `k` paths at any 66 vertex: the `r`-admissibility is at most `k`. -/ 67 def HasAdmAtMost {n : ℕ} (G : SimpleGraph (Fin n)) (r k : ℕ) : Prop := 68 ∃ π : Equiv.Perm (Fin n), ∀ (v : Fin n) (j : ℕ), 69 Nonempty (AdmFamily G π r j v) → j + 1 ≤ k 70 71 /-- The `r`-admissibility of `G`: the least bound achieved by some 72 vertex ordering. -/ 73 noncomputable def adm {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) : ℕ := 74 sInf {k | HasAdmAtMost G r k} 75 76 end Lax199508.Admissibility 77 -
Generalized coloring numbers
Fix a linear ordering of the vertices of a graph G. A vertex u is weakly r-reachable from v if some path from v to u of length at most r has u as its smallest vertex, and strongly r-reachable from v if some path from v to u of length at most r has v as its smallest vertex apart from u itself. The weak r-coloring number wcol_r(G) and the strong r-coloring number scol_r(G) are the minima, over all orderings, of the largest number of vertices weakly respectively strongly r-reachable from a single vertex. A graph class has subpolynomial weak coloring numbers if for every radius r and every ε > 0 there is a constant c such that every subgraph H of a member, on m vertices, satisfies wcol_r(H) ≤ c · m^ε.
Weak and strong reachability are Definition 2.1, and the two coloring numbers Definition 2.3, of Chapter 2 of the source lecture notes (2019/20 edition), which write scol_r where the earlier 2017/18 edition writes col_r. The subpolynomial bound is the conclusion of Theorem 3.4 of that chapter.
1 import Lax199508.GraphClasses 2 import Mathlib.Combinatorics.SimpleGraph.Copy 3 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic 4 import Mathlib.Data.Set.Card 5 import Mathlib.Data.Nat.Lattice 6 import Mathlib.Analysis.SpecialFunctions.Pow.Real 7 … module docstring, 47 lines 55 56 namespace Lax199508.ColoringNumbers 57 58 open scoped SimpleGraph 59 open Lax199508.GraphClasses 60 61 /-- The set of vertices weakly `r`-reachable from `v` in `G` under the 62 vertex ordering `π` (vertex `u` sits at position `π u`): the endpoints 63 `u` of walks from `v` of length at most `r` on whose support `u` is 64 `π`-minimal. Contains `v` itself. -/ 65 def wreach {n : ℕ} (G : SimpleGraph (Fin n)) (π : Equiv.Perm (Fin n)) 66 (r : ℕ) (v : Fin n) : Set (Fin n) := 67 {u | ∃ w : G.Walk v u, w.length ≤ r ∧ ∀ y ∈ w.support, π u ≤ π y} 68 69 /-- The set of vertices strongly `r`-reachable from `v` in `G` under the 70 vertex ordering `π`: the vertices `u` at or before `v` that are the 71 endpoint of a walk from `v` of length at most `r` all of whose other 72 vertices come strictly after `v`. Contains `v` itself. -/ 73 def sreach {n : ℕ} (G : SimpleGraph (Fin n)) (π : Equiv.Perm (Fin n)) 74 (r : ℕ) (v : Fin n) : Set (Fin n) := 75 {u | π u ≤ π v ∧ ∃ w : G.Walk v u, w.length ≤ r ∧ 76 ∀ y ∈ w.support, y ≠ v → y ≠ u → π v < π y} 77 78 /-- The weak `r`-coloring number of `G`: the least `k` such that under 79 some vertex ordering every vertex weakly `r`-reaches at most `k` 80 vertices. -/ 81 noncomputable def wcol {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) : ℕ := 82 sInf {k | ∃ π : Equiv.Perm (Fin n), ∀ v, (wreach G π r v).ncard ≤ k} 83 84 /-- The strong `r`-coloring number of `G`: the least `k` such that under 85 some vertex ordering every vertex strongly `r`-reaches at most `k` 86 vertices. -/ 87 noncomputable def scol {n : ℕ} (G : SimpleGraph (Fin n)) (r : ℕ) : ℕ := 88 sInf {k | ∃ π : Equiv.Perm (Fin n), ∀ v, (sreach G π r v).ncard ≤ k} 89 90 /-- Every subgraph of every member of the class, on `m` vertices, has 91 weak `r`-coloring number at most `c · m^ε`, where `c` depends only on 92 the radius `r` and on `ε > 0`: weak coloring numbers `m^{o(1)}`. -/ 93 def HasSubpolynomialWcol (C : GraphClass) : Prop := 94 ∀ (r : ℕ) (ε : ℝ), 0 < ε → ∃ c : ℝ, 95 ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → 96 ∀ (m : ℕ) (H : SimpleGraph (Fin m)), H ⊑ G → 97 (wcol H r : ℝ) ≤ c * (m : ℝ) ^ ε 98 99 end Lax199508.ColoringNumbers 100 -
Neighborhood complexity
The neighborhood complexity of a graph G on a vertex set A counts the distinct traces of vertex neighborhoods on A, that is, the sets N(v) ∩ A for v ranging over all vertices of G. A graph class has almost linear neighborhood complexity if for every ε > 0 there is a constant c such that every member G and every nonempty vertex subset A leave at most c · |A|^(1+ε) traces — neighborhood complexity |A|^(1+o(1)).
1 import Lax199508.GraphClasses 2 import Mathlib.Data.Set.Card 3 import Mathlib.Analysis.SpecialFunctions.Pow.Real 4 … module docstring, 34 lines 39 40 namespace Lax199508.NeighborhoodComplexity 41 42 open Lax199508.GraphClasses 43 44 /-- The number of distinct neighborhood traces `N(v) ∩ A` that the 45 vertices of `G` leave on the vertex set `A`. -/ 46 noncomputable def traceCount {V : Type*} (G : SimpleGraph V) 47 (A : Set V) : ℕ := 48 {S : Set V | ∃ v : V, S = G.neighborSet v ∩ A}.ncard 49 50 /-- Every graph in the class leaves at most `c · |A|^(1+ε)` neighborhood 51 traces on every nonempty vertex subset `A`, where `c` depends only on 52 `ε > 0`: neighborhood complexity `|A|^(1+o(1))`. -/ 53 def HasAlmostLinearNC (C : GraphClass) : Prop := 54 ∀ ε : ℝ, 0 < ε → ∃ c : ℝ, 55 ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → 56 ∀ A : Set (Fin n), A.Nonempty → 57 (traceCount G A : ℝ) ≤ c * (A.ncard : ℝ) ^ (1 + ε) 58 59 end Lax199508.NeighborhoodComplexity 60 -
Linear Neighbourhood Complexity
For a finite simple graph and a natural number , the neighbourhood complexity is the maximum, over sets of vertices, of the number of distinct traces on of the neighbourhoods of vertices outside . A graph class has linear neighbourhood complexity if is bounded by a constant multiple of for every positive .
1 import Lax9.MergeWidth 2 … module docstring, 11 lines 14 15 namespace Lax9.NeighborhoodComplexity 16 17 open Lax9.MergeWidth 18 open scoped Classical 19 20 universe u 21 22 variable {V : Type u} [Fintype V] 23 24 /-- The neighbourhood complexity of a finite simple graph . -/ 25 noncomputable def neighborhoodComplexity (G : SimpleGraph V) (p : ℕ) : ℕ := 26 (Finset.univ.powersetCard p).sup fun X => 27 ((Finset.univ \ X).image fun v => X.filter fun u => G.Adj v u).card 28 29 /-- A graph class has linear neighbourhood complexity if for 30 some constant and every positive . -/ 31 def LinearNeighborhoodComplexity (C : GraphClass) : Prop := 32 ∃ c : ℕ, ∀ ⦃V : Type⦄ [Fintype V] (G : SimpleGraph V), C G → ∀ p, 1 ≤ p → 33 neighborhoodComplexity G p ≤ c * p 34 35 end Lax9.NeighborhoodComplexity 36 -
Cographs
A finite graph is a cograph if it has twin-width zero. Equivalently, it can be reduced to one vertex by repeatedly contracting a pair of twins, without ever creating a red edge.
1 import Lax228581.TwinWidth 2 … module docstring, 17 lines 20 21 namespace Lax214022.Cographs 22 23 open Lax228581.TwinWidth 24 25 /-- A finite graph is a cograph when it admits a contraction sequence of red 26 degree zero. -/ 27 def IsCograph {V : Type} [Fintype V] [DecidableEq V] 28 (G : SimpleGraph V) : Prop := 29 HasTwinWidthAtMost G 0 30 31 end Lax214022.Cographs 32 -
Induced minors
A graph is an induced minor of if its vertices have pairwise disjoint, nonempty connected branch sets in , and two distinct branch sets are joined by an edge exactly when their vertices are adjacent in . Thus edges between retained branch sets cannot be deleted. For finite graphs this is the usual definition by vertex deletions and edge contractions.
1 import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected 2 … module docstring, 11 lines 14 15 namespace Lax762056.InducedMinors 16 17 open SimpleGraph 18 19 structure Model {W V : Type*} (H : SimpleGraph W) (G : SimpleGraph V) where 20 branch : W → Set V 21 connected : ∀ v, Connected (G.induce (branch v)) 22 disjoint : ∀ u v, u ≠ v → Disjoint (branch u) (branch v) 23 adjacent : ∀ u v, u ≠ v → 24 (H.Adj u v ↔ ∃ x ∈ branch u, ∃ y ∈ branch v, G.Adj x y) 25 26 def IsInducedMinor {W V : Type*} (H : SimpleGraph W) 27 (G : SimpleGraph V) : Prop := 28 Nonempty (Model H G) 29 30 end Lax762056.InducedMinors 31 -
Excluded induced grid minors
The square grid is the Cartesian product of two -vertex paths. A graph excludes the induced grid of size if this square grid is not an induced minor of the graph.
1 import Mathlib.Combinatorics.SimpleGraph.Hasse 2 import Lax762056.InducedMinors 3 … module docstring, 9 lines 13 14 namespace Lax762056.Grid 15 16 open SimpleGraph InducedMinors 17 18 def squareGrid (k : ℕ) : SimpleGraph (Fin k × Fin k) := 19 (pathGraph k).boxProd (pathGraph k) 20 21 def ExcludesInducedGrid (k : ℕ) {V : Type*} (G : SimpleGraph V) : Prop := 22 ¬ IsInducedMinor (squareGrid k) G 23 24 end Lax762056.Grid 25 -
Weakly sparse graph classes
A graph class is a set of finite simple graphs: for each number of vertices n, some of the simple graphs on the canonical n-element vertex type. A graph class is weakly sparse if some complete bipartite graph occurs in no member as a subgraph.
1 import Lax199508.GraphClasses 2 import Mathlib.Combinatorics.SimpleGraph.Copy 3 … module docstring, 26 lines 30 31 namespace Lax710763.GraphClasses 32 33 open scoped SimpleGraph 34 open Lax199508.GraphClasses 35 36 /-- The class of all finite simple graphs. -/ 37 def allGraphs : GraphClass := fun _ _ => True 38 39 /-- A graph class is weakly sparse if some complete bipartite graph 40 `K_{t,t}` occurs in no member as a subgraph. -/ 41 def WeaklySparse (C : GraphClass) : Prop := 42 ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → 43 ¬ completeBipartiteGraph (Fin t) (Fin t) ⊑ G 44 45 end Lax710763.GraphClasses 46 -
Graph minors
Graph minor illustration A graph H is a minor of a graph G when the vertices of H can be represented by pairwise disjoint connected branch sets in G, with an edge joining the corresponding branch sets for every edge of H.
1 import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected 2 … module docstring, 12 lines 15 16 set_option autoImplicit false 17 18 namespace Lax68.GraphMinors 19 20 structure MinorModel {W V : Type*} 21 (H : SimpleGraph W) (G : SimpleGraph V) where 22 branchSet : W → Set V 23 connected : ∀ w, (G.induce (branchSet w)).Connected 24 disjoint : 25 ∀ {u v}, u ≠ v → 26 Disjoint (branchSet u) (branchSet v) 27 adjacent : 28 ∀ {u v}, H.Adj u v → 29 ∃ x ∈ branchSet u, ∃ y ∈ branchSet v, G.Adj x y 30 31 def IsMinor {W V : Type*} 32 (H : SimpleGraph W) (G : SimpleGraph V) : Prop := 33 Nonempty (MinorModel H G) 34 35 abbrev K5 : SimpleGraph (Fin 5) := 36 SimpleGraph.completeGraph (Fin 5) 37 38 abbrev K4 : SimpleGraph (Fin 4) := 39 SimpleGraph.completeGraph (Fin 4) 40 41 abbrev K33 : SimpleGraph (Fin 3 ⊕ Fin 3) := 42 completeBipartiteGraph (Fin 3) (Fin 3) 43 44 abbrev K23 : SimpleGraph (Fin 2 ⊕ Fin 3) := 45 completeBipartiteGraph (Fin 2) (Fin 3) 46 47 end Lax68.GraphMinors 48 -
Topological graph minors
Topological minor illustration A graph H is a topological minor of G when the vertices of H are represented by distinct branch vertices of G and its edges by paths whose interiors contain no branch vertex and are pairwise disjoint. Equivalently, G contains a subdivision of H as a subgraph.
1 import Mathlib.Combinatorics.SimpleGraph.Paths 2 import Lax68.GraphMinors 3 … module docstring, 13 lines 17 18 set_option autoImplicit false 19 20 namespace Lax68.GraphTopologicalMinors 21 22 def walkInterior {V : Type*} {G : SimpleGraph V} {a b : V} 23 (P : G.Walk a b) : Set V := 24 {x | x ∈ P.support ∧ x ≠ a ∧ x ≠ b} 25 26 structure TopologicalMinorModel {W V : Type*} 27 (H : SimpleGraph W) (G : SimpleGraph V) where 28 branch : W ↪ V 29 route : 30 ∀ {a b : W}, H.Adj a b → 31 G.Walk (branch a) (branch b) 32 route_isPath : 33 ∀ {a b : W} (h : H.Adj a b), 34 (route h).IsPath 35 branch_avoids_interiors : 36 ∀ {a b : W} (h : H.Adj a b) (w : W), 37 branch w ∉ walkInterior (route h) 38 route_interiors_disjoint : 39 ∀ {a b c d : W} 40 (hab : H.Adj a b) (hcd : H.Adj c d), 41 ¬ ((a = c ∧ b = d) ∨ (a = d ∧ b = c)) → 42 Disjoint 43 (walkInterior (route hab)) 44 (walkInterior (route hcd)) 45 46 def IsTopologicalMinor {W V : Type*} 47 (H : SimpleGraph W) (G : SimpleGraph V) : Prop := 48 Nonempty (TopologicalMinorModel H G) 49 50 def IsKuratowskiFree {V : Type*} (G : SimpleGraph V) : Prop := 51 ¬IsTopologicalMinor Lax68.GraphMinors.K5 G ∧ 52 ¬IsTopologicalMinor Lax68.GraphMinors.K33 G 53 54 end Lax68.GraphTopologicalMinors 55 -
Grids and walls
Grid and wall illustration A nonempty rectangular grid has vertices in rows and columns, with edges between orthogonally consecutive positions. A wall is the brick-wall subgraph obtained by retaining alternating vertical grid edges.
1 import Mathlib.Combinatorics.SimpleGraph.Hasse 2 … module docstring, 12 lines 15 16 set_option autoImplicit false 17 18 namespace Lax68.GridsAndWalls 19 20 def consecutive (a b : ℕ) : Prop := 21 a + 1 = b ∨ b + 1 = a 22 23 def WallAdjacent {m n : ℕ} (u v : Fin m × Fin n) : Prop := 24 (u.1 = v.1 ∧ consecutive u.2.val v.2.val) ∨ 25 (u.2 = v.2 ∧ 26 consecutive u.1.val v.1.val ∧ 27 (Nat.min u.1.val v.1.val + u.2.val) % 2 = 0) 28 29 def HasGridShape {V : Type*} (G : SimpleGraph V) : Prop := 30 ∃ m n : ℕ, 31 0 < m ∧ 32 0 < n ∧ 33 Nonempty 34 (G ≃g (SimpleGraph.pathGraph m □ SimpleGraph.pathGraph n)) 35 36 def HasWallShape {V : Type*} (G : SimpleGraph V) : Prop := 37 ∃ m n : ℕ, 38 0 < m ∧ 39 0 < n ∧ 40 ∃ e : Fin m × Fin n ≃ V, 41 ∀ u v, 42 G.Adj (e u) (e v) ↔ WallAdjacent u v 43 44 def IsGrid {V : Type*} (G : SimpleGraph V) : Prop := 45 HasGridShape G 46 47 def IsWall {V : Type*} (G : SimpleGraph V) : Prop := 48 HasWallShape G 49 50 end Lax68.GridsAndWalls 51 -
Outerplanar graphs
Outerplanar graph illustration A graph is outerplanar here when it has a crossing-free straight-line drawing with every vertex on one circle, a compact certificate for having every vertex on the boundary of the outer face.
1 import Lax68.GraphMinors 2 import Lax68.StraightLineDrawings 3 … module docstring, 12 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.Outerplanar 20 21 structure OuterplaneDrawing {V : Type*} (G : SimpleGraph V) 22 extends StraightLineDrawings.StraightLineDrawing G where 23 radius : ℝ 24 radius_pos : 0 < radius 25 onBoundary : 26 ∀ v : V, 27 let p := toStraightLineDrawing.point v 28 p.1 ^ 2 + p.2 ^ 2 = radius ^ 2 29 30 def IsOuterplanar {V : Type*} (G : SimpleGraph V) : Prop := 31 Nonempty (OuterplaneDrawing G) 32 33 /-- The usual forbidden-minor characterization of outerplanarity. -/ 34 def IsOuterplanarByExcludedMinors {V : Type*} (G : SimpleGraph V) : Prop := 35 ¬ GraphMinors.IsMinor GraphMinors.K4 G ∧ 36 ¬ GraphMinors.IsMinor GraphMinors.K23 G 37 38 end Lax68.Outerplanar 39 -
def
Lax68.PlanarPlanar graphs
Planar graph illustration A graph is planar here when it has a crossing-free straight-line drawing in the real plane. For finite simple graphs, this agrees with the usual notion of planarity. The drawing certificate is supplied by a separate concept.
1 import Lax68.GraphMinors 2 import Lax68.StraightLineDrawings 3 … module docstring, 12 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.Planar 20 21 /-- Existence of a crossing-free straight-line drawing in the real plane. -/ 22 def IsPlanar {V : Type*} (G : SimpleGraph V) : Prop := 23 StraightLineDrawings.HasStraightLineDrawing G 24 25 def IsPlanarByExcludedMinors {V : Type*} (G : SimpleGraph V) : Prop := 26 ¬GraphMinors.IsMinor GraphMinors.K5 G ∧ 27 ¬GraphMinors.IsMinor GraphMinors.K33 G 28 29 end Lax68.Planar 30 -
Triangulations
Triangulation illustration A triangulation of a graph G is a planar supergraph T on the same vertex set, with at least three vertices, to which no edge can be added while preserving planarity. For a plane embedding this is equivalent to every face of T being bounded by a triangle.
1 import Lax68.Planar 2 … module docstring, 13 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.Triangulations 20 21 def IsTriangulationOf {V : Type*} 22 (G T : SimpleGraph V) : Prop := 23 (∃ a b c : V, a ≠ b ∧ a ≠ c ∧ b ≠ c) ∧ 24 G ≤ T ∧ 25 Planar.IsPlanar T ∧ 26 ∀ H : SimpleGraph V, 27 T < H → 28 ¬ Planar.IsPlanar H 29 30 end Lax68.Triangulations 31 -
Mixed minor number
A k-division of partitions it into k nonempty consecutive intervals in increasing order. A row division and a column division split a matrix into a grid of k² cells. A cell is vertical if each of its columns is constant, horizontal if each of its rows is constant, and mixed if it is neither. The matrix has a k-mixed minor if some pair of row and column k-divisions makes all k² cells mixed, and its mixed number is the largest such k.
An ordering of a finite simple graph's vertices turns its adjacency relation into such a matrix. The mixed minor number of the graph is the least mixed number of this matrix over all vertex orderings.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 import Mathlib.Data.Nat.Lattice 3 … module docstring, 28 lines 32 33 namespace Lax153141.MixedMinorNumber 34 35 /-- A division of `Fin n` into `k` nonempty consecutive intervals in 36 increasing order. Disjointness and convexity of the parts follow from 37 `part_ordered` and `part_cover`. -/ 38 structure Division (n k : ℕ) where 39 /-- The `i`-th part of the division. -/ 40 part : Fin k → Finset (Fin n) 41 /-- Every part is nonempty. -/ 42 part_nonempty : ∀ i, (part i).Nonempty 43 /-- The parts cover the whole interval. -/ 44 part_cover : ∀ x : Fin n, ∃ i, x ∈ part i 45 /-- Earlier-indexed parts lie strictly before later-indexed parts. -/ 46 part_ordered : 47 ∀ ⦃i j : Fin k⦄, i < j → 48 ∀ ⦃a b : Fin n⦄, a ∈ part i → b ∈ part j → a < b 49 50 /-- A matrix cell is vertical when each column is constant within the row 51 part. -/ 52 def cellVertical {n m k : ℕ} (M : Fin n → Fin m → Prop) 53 (R : Division n k) (C : Division m k) (i j : Fin k) : Prop := 54 ∀ ⦃r₁ r₂ : Fin n⦄, r₁ ∈ R.part i → r₂ ∈ R.part i → 55 ∀ ⦃c : Fin m⦄, c ∈ C.part j → (M r₁ c ↔ M r₂ c) 56 57 /-- A matrix cell is horizontal when each row is constant within the column 58 part. -/ 59 def cellHorizontal {n m k : ℕ} (M : Fin n → Fin m → Prop) 60 (R : Division n k) (C : Division m k) (i j : Fin k) : Prop := 61 ∀ ⦃r : Fin n⦄, r ∈ R.part i → 62 ∀ ⦃c₁ c₂ : Fin m⦄, c₁ ∈ C.part j → c₂ ∈ C.part j → 63 (M r c₁ ↔ M r c₂) 64 65 /-- A matrix cell is mixed when it is neither vertical nor horizontal. -/ 66 def cellMixed {n m k : ℕ} (M : Fin n → Fin m → Prop) 67 (R : Division n k) (C : Division m k) (i j : Fin k) : Prop := 68 ¬ cellVertical M R C i j ∧ ¬ cellHorizontal M R C i j 69 70 /-- A matrix has a `k`-mixed minor if suitable row and column `k`-divisions 71 make every induced cell mixed. -/ 72 def HasMixedMinor {n m : ℕ} (M : Fin n → Fin m → Prop) (k : ℕ) : Prop := 73 ∃ R : Division n k, ∃ C : Division m k, ∀ i j : Fin k, cellMixed M R C i j 74 75 /-- The largest order of a mixed minor of a matrix. -/ 76 noncomputable def matrixMixedNumber {n m : ℕ} 77 (M : Fin n → Fin m → Prop) : ℕ := 78 sSup {k | HasMixedMinor M k} 79 80 /-- The adjacency matrix of a graph in a chosen vertex order. -/ 81 def orderedAdjacency {V : Type} {n : ℕ} 82 (G : SimpleGraph V) (e : Fin n ≃ V) : Fin n → Fin n → Prop := 83 fun i j => G.Adj (e i) (e j) 84 85 /-- The mixed minor number of a finite simple graph: the least mixed number 86 of its adjacency matrix over all vertex orderings. -/ 87 noncomputable def mixedMinorNumber {V : Type} [Fintype V] [DecidableEq V] 88 (G : SimpleGraph V) : ℕ := 89 sInf (Set.range fun e : Fin (Fintype.card V) ≃ V => 90 matrixMixedNumber (orderedAdjacency G e)) 91 92 end Lax153141.MixedMinorNumber 93 -
Uniform quasi-wideness
A set A of vertices is distance-r independent in G if any two distinct vertices of A are at distance more than r. A graph class is uniformly quasi-wide if for every radius r there are a threshold function N and a separator bound s such that in every member G, every vertex set A of size at least N(m) contains a distance-r independent subset of size at least m of G − S, for some set S of at most s vertices.
This is Definition 3.1 of Chapter 4 of the source lecture notes (2019/20 edition), where the constants s are called the margins and the functions N the wideness functions.
1 import Lax199508.GraphClasses 2 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic 3 import Mathlib.Data.Set.Card 4 … module docstring, 37 lines 42 43 namespace Lax199508.UniformQuasiWideness 44 45 open Lax199508.GraphClasses 46 47 /-- A set of vertices is distance-`r` independent in `G` when every walk 48 between two distinct members is longer than `r`. -/ 49 def DistIndependent {V : Type*} (G : SimpleGraph V) (r : ℕ) (A : Set V) : Prop := 50 A.Pairwise fun u v => ∀ p : G.Walk u v, r < p.length 51 52 /-- `G` with the vertices of `S` isolated: every edge incident to `S` is 53 removed and the vertex type is unchanged. This models `G − S`. -/ 54 def deleteVerts {V : Type*} (G : SimpleGraph V) (S : Set V) : SimpleGraph V where 55 Adj u v := G.Adj u v ∧ u ∉ S ∧ v ∉ S 56 symm := ⟨by 57 intro u v h 58 exact ⟨h.1.symm, h.2.2, h.2.1⟩⟩ 59 loopless := ⟨fun v h => G.loopless.irrefl v h.1⟩ 60 61 /-- A graph class is uniformly quasi-wide if for every radius `r` there 62 are a threshold function `N` and a separator bound `s` such that in 63 every member, every vertex set of size at least `N m` contains a 64 distance-`r` independent subset of size at least `m` after deleting at 65 most `s` vertices. -/ 66 def UniformlyQuasiWide (C : GraphClass) : Prop := 67 ∀ r : ℕ, ∃ (N : ℕ → ℕ) (s : ℕ), 68 ∀ (m n : ℕ) (G : SimpleGraph (Fin n)), C n G → 69 ∀ A : Set (Fin n), N m ≤ A.ncard → 70 ∃ S B : Set (Fin n), 71 S.ncard ≤ s ∧ B ⊆ A \ S ∧ m ≤ B.ncard ∧ 72 DistIndependent (deleteVerts G S) r B 73 74 end Lax199508.UniformQuasiWideness 75 -
Edge density of shallow minors
A graph G has depth-r density at most d if every depth-r minor H of G has at most d · |V(H)| edges — the standard "grad" bound on how dense the shallow minors of a sparse graph can be. A graph class has subpolynomial density if for every depth r and every ε > 0 there is a constant c such that every depth-r minor H of a member, on m vertices, has at most c · m^(1+ε) edges: shallow-minor edge counts m^(1+o(1)).
Definition 2.4 of Chapter 1 of the source lecture notes (2019/20 edition) defines the grad ∇r(G) as the supremum of |E(H)|/|V(H)| over the depth-r minors H of G, so the per-graph predicate here says ∇r(G) ≤ d.
1 import Lax199508.NowhereDenseClasses 2 import Mathlib.Data.Set.Card 3 import Mathlib.Analysis.SpecialFunctions.Pow.Real 4 … module docstring, 41 lines 46 47 namespace Lax199508.ShallowMinorDensity 48 49 open Lax199508.GraphClasses Lax199508.NowhereDenseClasses 50 51 /-- Every depth-`r` minor of `G`, on `m` vertices, has at most `d · m` 52 edges. -/ 53 def HasDensityAtMost {n : ℕ} (G : SimpleGraph (Fin n)) (r d : ℕ) : Prop := 54 ∀ (m : ℕ) (H : SimpleGraph (Fin m)), HasShallowMinor G r H → 55 H.edgeSet.ncard ≤ d * m 56 57 /-- Every depth-`r` minor of every member of the class, on `m` vertices, 58 has at most `c · m^(1+ε)` edges, where `c` depends only on the depth `r` 59 and on `ε > 0`: shallow-minor edge counts `m^(1+o(1))`. -/ 60 def HasSubpolynomialDensity (C : GraphClass) : Prop := 61 ∀ (r : ℕ) (ε : ℝ), 0 < ε → ∃ c : ℝ, 62 ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → 63 ∀ (m : ℕ) (H : SimpleGraph (Fin m)), HasShallowMinor G r H → 64 (H.edgeSet.ncard : ℝ) ≤ c * (m : ℝ) ^ (1 + ε) 65 66 end Lax199508.ShallowMinorDensity 67 -
Shallow topological minors
A graph H is a depth-r topological minor of a graph G if the graph obtained from H by subdividing every edge at most 2r times is a subgraph of G: the vertices of H are realized by distinct principal vertices of G, and every edge of H by a path of length at most 2r+1 between the principal vertices of its endpoints, these paths being internally disjoint from each other and from all principal vertices. A graph G has depth-r topological density at most d if every depth-r topological minor H of G has at most d · |V(H)| edges.
In the source lecture notes these are Definitions 2.15 and 2.16 of Chapter 1 (2019/20 edition): the topological minor relation is written H ⪯^top_r G, and the topological grad ∇̃_r(G) is the supremum of |E(H)|/|V(H)| over the depth-r topological minors H of G, so the density predicate here says ∇̃_r(G) ≤ d. The length bound 2r+1 is the notes' own convention, chosen so that a depth-r topological minor is in particular a depth-r minor.
1 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic 2 import Mathlib.Data.Set.Card 3 … module docstring, 59 lines 63 64 namespace Lax199508.ShallowTopologicalMinors 65 66 /-- A model of `H` as a depth-`r` topological minor of `G`: an injective 67 choice of a principal vertex of `G` for each vertex of `H`, together 68 with a connecting walk of length at most `2 * r + 1` for each edge of 69 `H`, where the walks pass through no principal vertex other than those 70 of their own two endpoints and meet each other only in principal 71 vertices. -/ 72 structure ShallowTopologicalMinorModel {V W : Type*} (r : ℕ) (H : SimpleGraph W) 73 (G : SimpleGraph V) where 74 /-- The principal vertex of `G` realizing each vertex of `H`. -/ 75 principal : W → V 76 /-- Distinct vertices of `H` have distinct principal vertices. -/ 77 principal_inj : Function.Injective principal 78 /-- The walk of `G` connecting the principal vertices of an edge of 79 `H`. -/ 80 walk : ∀ (u v : W), H.Adj u v → G.Walk (principal u) (principal v) 81 /-- Connecting walks have length at most `2 * r + 1`: they subdivide 82 the edge at most `2 * r` times. -/ 83 length_le : ∀ (u v : W) (h : H.Adj u v), (walk u v h).length ≤ 2 * r + 1 84 /-- A principal vertex lying on a connecting walk is one of the two 85 endpoints of that edge. -/ 86 principal_eq : ∀ (u v : W) (h : H.Adj u v) (w : W), 87 principal w ∈ (walk u v h).support → w = u ∨ w = v 88 /-- Connecting walks meet only in principal vertices: a vertex lying 89 on two connecting walks and on none of the principal vertices forces 90 the two edges to agree. -/ 91 disjoint : ∀ (u v : W) (h : H.Adj u v) (u' v' : W) (h' : H.Adj u' v') (x : V), 92 x ∈ (walk u v h).support → x ∈ (walk u' v' h').support → 93 x ∉ Set.range principal → (u = u' ∧ v = v') ∨ (u = v' ∧ v = u') 94 95 /-- `H` is a topological minor of `G` at depth `r`. -/ 96 def HasShallowTopologicalMinor {V W : Type*} (G : SimpleGraph V) (r : ℕ) 97 (H : SimpleGraph W) : Prop := 98 Nonempty (ShallowTopologicalMinorModel r H G) 99 100 /-- Every depth-`r` topological minor of `G`, on `m` vertices, has at 101 most `d · m` edges. -/ 102 def HasTopologicalDensityAtMost {n : ℕ} (G : SimpleGraph (Fin n)) (r d : ℕ) : 103 Prop := 104 ∀ (m : ℕ) (H : SimpleGraph (Fin m)), HasShallowTopologicalMinor G r H → 105 H.edgeSet.ncard ≤ d * m 106 107 end Lax199508.ShallowTopologicalMinors 108 -
Nowhere dense graph classes
A graph H is a depth-r minor of a graph G if H can be obtained from G by deleting vertices and edges and contracting pairwise disjoint connected subgraphs of radius at most r. A graph class is nowhere dense if for every depth r there is a t such that no member has the complete graph on t vertices as a depth-r minor.
The source lecture notes give these as Definitions 2.3 and 2.6 of Chapter 1 (2019/20 edition), writing H ⪯r G for the depth-r minor relation. Nowhere denseness is stated there as ωr(C) < ∞ for every r, with the excluded-clique form used here spelled out immediately after as an equivalent.
1 import Lax199508.GraphClasses 2 import Mathlib.Combinatorics.SimpleGraph.Walk.Basic 3 … module docstring, 29 lines 33 34 namespace Lax199508.NowhereDenseClasses 35 36 open Lax199508.GraphClasses 37 38 /-- A model of `H` as a depth-`r` minor of `G`: pairwise disjoint branch 39 sets, each spanned by walks of length at most `r` from a center vertex 40 (hence connected of radius at most `r`), with an edge of `G` between the 41 branch sets of any two adjacent vertices of `H`. -/ 42 structure ShallowMinorModel {V W : Type*} (r : ℕ) (H : SimpleGraph W) 43 (G : SimpleGraph V) where 44 /-- The branch set of each vertex of `H`. -/ 45 branch : W → Set V 46 /-- The center of each branch set. -/ 47 center : W → V 48 /-- Centers lie in their branch sets (so branch sets are nonempty). -/ 49 center_mem : ∀ u, center u ∈ branch u 50 /-- Distinct branch sets are disjoint. -/ 51 disjoint : ∀ u v, u ≠ v → Disjoint (branch u) (branch v) 52 /-- Every vertex of a branch set is reached from the center by a walk 53 of length at most `r` inside the branch set. -/ 54 radius_le : ∀ u, ∀ x ∈ branch u, ∃ w : G.Walk (center u) x, 55 w.length ≤ r ∧ ∀ y ∈ w.support, y ∈ branch u 56 /-- Adjacent vertices of `H` have adjacent branch sets. -/ 57 adj : ∀ u v, H.Adj u v → ∃ x ∈ branch u, ∃ y ∈ branch v, G.Adj x y 58 59 /-- `H` is a minor of `G` at depth `r`. -/ 60 def HasShallowMinor {V W : Type*} (G : SimpleGraph V) (r : ℕ) 61 (H : SimpleGraph W) : Prop := 62 Nonempty (ShallowMinorModel r H G) 63 64 /-- A graph class is nowhere dense if for every depth `r` some complete 65 graph is not a depth-`r` minor of any member. -/ 66 def NowhereDense (C : GraphClass) : Prop := 67 ∀ r : ℕ, ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → 68 ¬ HasShallowMinor G r (⊤ : SimpleGraph (Fin t)) 69 70 end Lax199508.NowhereDenseClasses 71 -
Monadic dependence
A graph class is monadically dependent (also called monadically NIP) if it does not transduce the class of all graphs.
1 import Lax710763.GraphClasses 2 import Lax710763.GraphTransductions 3 … module docstring, 14 lines 18 19 namespace Lax710763.MonadicDependence 20 21 open Lax199508.GraphClasses Lax710763.GraphClasses 22 23 /-- A graph class is monadically dependent if it does not transduce the 24 class of all finite simple graphs. -/ 25 def MonadicallyDependent (C : GraphClass) : Prop := 26 ¬ GraphTransductions.Transduces C allGraphs 27 28 end Lax710763.MonadicDependence 29 -
def
Lax68.TreesTrees
Tree illustration A tree is a connected acyclic simple graph, using mathlib's native predicate.
1 import Mathlib.Combinatorics.SimpleGraph.Acyclic 2 … module docstring, 11 lines 14 15 set_option autoImplicit false 16 17 namespace Lax68.Trees 18 19 def IsTree {V : Type*} (G : SimpleGraph V) : Prop := 20 G.IsTree 21 22 end Lax68.Trees 23 -
Treewidth
A tree decomposition of a finite simple graph G consists of a finite tree T and a bag of graph vertices at each node such that every graph vertex occurs in a bag, the endpoints of every graph edge occur together in a bag, and the nodes whose bags contain any fixed vertex induce a connected subgraph of T.
The treewidth of G is the least w such that G has a tree decomposition with every bag of size at most w + 1.
1 import Mathlib.Combinatorics.SimpleGraph.Acyclic 2 import Mathlib.Data.Nat.Lattice 3 … module docstring, 21 lines 25 26 namespace Lax228581.Treewidth 27 28 /-- A tree decomposition of a simple graph: a finite tree of nodes with a bag 29 of graph vertices at each node, such that the bags cover every vertex and 30 every edge, and the nodes whose bags contain any fixed vertex induce a 31 connected subgraph of the tree. -/ 32 structure TreeDecomposition {V : Type} (G : SimpleGraph V) where 33 /-- The node type of the decomposition tree. -/ 34 Node : Type 35 /-- The decomposition tree is finite. -/ 36 [nodeFintype : Fintype Node] 37 /-- The graph on the decomposition nodes. -/ 38 tree : SimpleGraph Node 39 /-- The node graph is a tree. -/ 40 isTree : tree.IsTree 41 /-- The bag assigned to each decomposition node. -/ 42 bag : Node → Finset V 43 /-- Every graph vertex appears in at least one bag. -/ 44 vertex_mem_bag : ∀ v : V, ∃ i : Node, v ∈ bag i 45 /-- Every graph edge has both endpoints together in at least one bag. -/ 46 edge_mem_bag : ∀ ⦃u v : V⦄, G.Adj u v → ∃ i : Node, u ∈ bag i ∧ v ∈ bag i 47 /-- For each graph vertex, the nodes whose bags contain it induce a 48 connected subgraph of the tree. -/ 49 bag_indices_connected : 50 ∀ v : V, (tree.induce {i : Node | v ∈ bag i}).Connected 51 52 /-- `G` has a tree decomposition all of whose bags have at most `w + 1` 53 vertices. -/ 54 def HasTreewidthAtMost {V : Type} (G : SimpleGraph V) (w : ℕ) : Prop := 55 ∃ D : TreeDecomposition G, ∀ i, (D.bag i).card ≤ w + 1 56 57 /-- The treewidth of a finite simple graph: the least `w` such that the 58 graph has a tree decomposition with bags of at most `w + 1` vertices. -/ 59 noncomputable def treewidth {V : Type} [Fintype V] [DecidableEq V] 60 (G : SimpleGraph V) : ℕ := 61 sInf {w | HasTreewidthAtMost G w} 62 63 end Lax228581.Treewidth 64 -
Series-parallel graphs
Series-parallel graph illustration A finite two-terminal series-parallel graph is built from a single terminal edge by series and parallel composition. The side conditions say that the composed graphs meet only at the intended terminals, and the final support condition excludes unused isolated vertices.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 … module docstring, 13 lines 16 17 set_option autoImplicit false 18 19 namespace Lax68.SeriesParallel 20 21 def edgeGraph {V : Type*} (s t : V) : SimpleGraph V := 22 SimpleGraph.fromRel fun u v => 23 (u = s ∧ v = t) ∨ 24 (u = t ∧ v = s) 25 26 inductive TwoTerminal {V : Type*} : SimpleGraph V → V → V → Prop 27 | edge (s t : V) (hne : s ≠ t) : 28 TwoTerminal (edgeGraph s t) s t 29 | series 30 {G H : SimpleGraph V} 31 {s m t : V} 32 (left : TwoTerminal G s m) 33 (right : TwoTerminal H m t) 34 (meet : 35 ∀ v, 36 v ∈ G.support → 37 v ∈ H.support → 38 v = m) : 39 TwoTerminal (G ⊔ H) s t 40 | parallel 41 {G H : SimpleGraph V} 42 {s t : V} 43 (left : TwoTerminal G s t) 44 (right : TwoTerminal H s t) 45 (meet : 46 ∀ v, 47 v ∈ G.support → 48 v ∈ H.support → 49 v = s ∨ v = t) : 50 TwoTerminal (G ⊔ H) s t 51 52 def IsSeriesParallel {V : Type*} (G : SimpleGraph V) : Prop := 53 ∃ s t, 54 TwoTerminal G s t ∧ 55 G.support = Set.univ 56 57 end Lax68.SeriesParallel 58 -
Cographs
A finite graph is a cograph if it has twin-width zero. Equivalently, it can be reduced to one vertex by repeatedly contracting a pair of twins, without ever creating a red edge.
1 import Lax228581.TwinWidth 2 … module docstring, 17 lines 20 21 namespace Lax214022.Cographs 22 23 open Lax228581.TwinWidth 24 25 /-- A finite graph is a cograph when it admits a contraction sequence of red 26 degree zero. -/ 27 def IsCograph {V : Type} [Fintype V] [DecidableEq V] 28 (G : SimpleGraph V) : Prop := 29 HasTwinWidthAtMost G 0 30 31 end Lax214022.Cographs 32 -
k-expressions, and the graphs of cliquewidth at most k
A k-expression builds a graph from single vertices, each created with one of k labels, by three operations: disjoint union of two expressions; adding every edge between the vertices of one label class and those of another; and relabelling, which moves one label class into another. Evaluating an expression gives a vertex set, a graph on it, and the k label classes it has arrived at. A graph has cliquewidth at most k when some k-expression evaluates to it — that is the width measure the theorem below is stated for, and an expression for the graph is what the theorem takes as input.
An expression is valid when its leaves create pairwise distinct vertices and every edge-adding operation joins two different classes; it is an expression for a graph when in addition its leaves create all of 's vertices and it evaluates to exactly 's edges.
The operations of an expression are also numbered here, since the numbers are what a machine reading an expression is handed: the disjoint union is , creating a vertex with label is , and the two binary operations occupy two further blocks of numbers each, in which a pair of labels is read in base .
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 … module docstring, 61 lines 64 65 namespace Lax271696.CliqueExpr 66 67 variable {n k : ℕ} 68 69 /-- A `k`-expression over the vertex names `Fin n`: a single labelled 70 vertex, disjoint union, edge addition between two label classes, or 71 relabelling one class into another. -/ 72 inductive Expr (n k : ℕ) : Type 73 /-- The vertex `v`, carrying label `l`. -/ 74 | leaf (v : Fin n) (l : Fin k) 75 /-- Disjoint union `⊕`. -/ 76 | union (e₁ e₂ : Expr n k) 77 /-- `η i j`: join every vertex of class `i` to every vertex of class `j`. -/ 78 | addEdges (i j : Fin k) (e : Expr n k) 79 /-- `ρ i j`: move class `i` into class `j`. -/ 80 | relabel (i j : Fin k) (e : Expr n k) 81 82 /-- The vertex names created by the leaves, in order. -/ 83 def leafIds : Expr n k → List (Fin n) 84 | .leaf v _ => [v] 85 | .union e₁ e₂ => leafIds e₁ ++ leafIds e₂ 86 | .addEdges _ _ e => leafIds e 87 | .relabel _ _ e => leafIds e 88 89 /-- The vertex set of an expression. -/ 90 def verts : Expr n k → Finset (Fin n) 91 | .leaf v _ => {v} 92 | .union e₁ e₂ => verts e₁ ∪ verts e₂ 93 | .addEdges _ _ e => verts e 94 | .relabel _ _ e => verts e 95 96 /-- The label classes of an expression: `cls e i` is the set of vertices 97 of `e` currently carrying label `i`. -/ 98 def cls : Expr n k → Fin k → Finset (Fin n) 99 | .leaf v l, i => if i = l then {v} else ∅ 100 | .union e₁ e₂, i => cls e₁ i ∪ cls e₂ i 101 | .addEdges _ _ e, i => cls e i 102 | .relabel i j e, t => if t = j then cls e i ∪ cls e j else if t = i then ∅ else cls e t 103 104 /-- The graph an expression evaluates to. -/ 105 def graph : Expr n k → SimpleGraph (Fin n) 106 | .leaf _ _ => ⊥ 107 | .union e₁ e₂ => graph e₁ ⊔ graph e₂ 108 | .addEdges i j e => graph e ⊔ SimpleGraph.fromRel fun u v => u ∈ cls e i ∧ v ∈ cls e j 109 | .relabel _ _ e => graph e 110 111 /-- The evaluated graph has a decidable adjacency relation, by the same 112 structural recursion. -/ 113 instance decidableAdj : ∀ e : Expr n k, DecidableRel (graph e).Adj 114 | .leaf _ _ => inferInstanceAs (DecidableRel (⊥ : SimpleGraph (Fin n)).Adj) 115 | .union e₁ e₂ => 116 have := decidableAdj e₁ 117 have := decidableAdj e₂ 118 inferInstanceAs (DecidableRel (graph e₁ ⊔ graph e₂).Adj) 119 | .addEdges i j e => 120 have := decidableAdj e 121 inferInstanceAs (DecidableRel 122 (graph e ⊔ SimpleGraph.fromRel fun u v => u ∈ cls e i ∧ v ∈ cls e j).Adj) 123 | .relabel _ _ e => decidableAdj e 124 125 /-- Well-formedness of the operations: `addEdges` joins two *different* 126 classes, the standard restriction on `η`. -/ 127 def opsOk : Expr n k → Bool 128 | .leaf _ _ => true 129 | .union e₁ e₂ => opsOk e₁ && opsOk e₂ 130 | .addEdges i j e => (i != j) && opsOk e 131 | .relabel _ _ e => opsOk e 132 133 /-- A valid expression: the leaves create pairwise distinct vertices — 134 which is what makes the two sides of every `⊕` disjoint — and the 135 operations are well formed. -/ 136 structure Valid (e : Expr n k) : Prop where 137 /-- No vertex name is created twice. -/ 138 nodup : (leafIds e).Nodup 139 /-- Every `addEdges` joins two different classes. -/ 140 ops : opsOk e = true 141 142 /-- A `k`-expression *for* `G`: valid, and at the root it has created 143 every vertex and exactly the edges of `G`. -/ 144 structure ValidFor (e : Expr n k) (G : SimpleGraph (Fin n)) : Prop extends Valid e where 145 /-- The root creates every vertex. -/ 146 verts_eq : verts e = Finset.univ 147 /-- The root evaluates to `G`. -/ 148 graph_eq : graph e = G 149 150 /-- The operation performed at a node of a `k`-expression. -/ 151 inductive Op (k : ℕ) where 152 /-- Disjoint union. -/ 153 | union 154 /-- Create a vertex with label `l`. -/ 155 | leaf (l : Fin k) 156 /-- `η i j`: join class `i` to class `j`. -/ 157 | eta (i j : Fin k) 158 /-- `ρ i j`: move class `i` into class `j`. -/ 159 | rho (i j : Fin k) 160 deriving DecidableEq 161 162 /-- The number naming an operation. The blocks are `union` (one code), 163 the leaves (`k` codes), the joins and the relabels (`k²` codes each, 164 the pair `(i, j)` read in base `k`). -/ 165 def Op.code : Op k → ℕ 166 | .union => 0 167 | .leaf l => 1 + (l : ℕ) 168 | .eta i j => 1 + k + ((i : ℕ) * k + (j : ℕ)) 169 | .rho i j => 1 + k + k * k + ((i : ℕ) * k + (j : ℕ)) 170 171 /-- The size of the operation alphabet. -/ 172 def opCard (k : ℕ) : ℕ := 1 + k + 2 * (k * k) 173 174 end Lax271696.CliqueExpr 175 -
Merge-Width
A merge sequence of a finite simple graph consists of a coarsening sequence of partitions and a monotone sequence of graphs of resolved pairs. At each step, adjacency is uniform on the unresolved pairs between any two parts. The radius- width of a merge sequence is the maximum number of parts of the preceding partition met by a radius- ball in the graph of resolved pairs. The radius- merge-width of a graph is the minimum width of a merge sequence of that graph. A graph class has bounded merge-width if these parameters are bounded by a function of throughout the class.
1 import Mathlib 2 … module docstring, 14 lines 17 18 namespace Lax9.MergeWidth 19 20 open scoped Classical 21 22 universe u 23 24 variable {V : Type u} [Fintype V] 25 26 /-- The **resolved ball** of radius around in a graph : 27 the set of vertices reachable from by a walk of length at most . 28 In the paper this is applied to the graph of resolved pairs. -/ 29 def resolvedBall (H : SimpleGraph V) (r : ℕ) (v : V) : Set V := 30 {u | ∃ w : H.Walk v u, w.length ≤ r} 31 32 /-- 33 A **merge sequence** for a finite simple graph is a sequence 34 where: 35 36 * each is a partition of (encoded as a ), with 37 the partition into singletons () and the trivial partition 38 with one part (); 39 * the partitions are **coarsening**: for 40 (recall that for setoids a *coarser* partition is a *larger* relation); 41 * each is the graph of **resolved pairs**, and these are 42 **monotone**: for ; 43 * (**uniformity**) for any two parts of , the *unresolved* pairs 44 between and (pairs ) are either all edges or all non-edges of 45 . 46 -/ 47 structure MergeSeq (G : SimpleGraph V) where 48 /-- The number of steps of the sequence. -/ 49 length : ℕ 50 /-- The sequence is nonempty. -/ 51 one_le_length : 1 ≤ length 52 /-- The partition at step (as a setoid on the vertices). -/ 53 part : ℕ → Setoid V 54 /-- The graph of resolved pairs at step . -/ 55 resolved : ℕ → SimpleGraph V 56 /-- is the partition into singletons. -/ 57 part_one : part 1 = ⊥ 58 /-- is the trivial partition with a single part. -/ 59 part_length : part length = ⊤ 60 /-- The partitions get coarser. -/ 61 part_mono : ∀ ⦃i j⦄, 1 ≤ i → i ≤ j → j ≤ length → part i ≤ part j 62 /-- The sets of resolved pairs are monotone. -/ 63 resolved_mono : ∀ ⦃i j⦄, 1 ≤ i → i ≤ j → j ≤ length → resolved i ≤ resolved j 64 /-- Uniformity: unresolved pairs between two parts are all edges or all 65 non-edges. -/ 66 uniform : ∀ ⦃i⦄, 1 ≤ i → i ≤ length → ∀ ⦃x x' y y' : V⦄, 67 (part i).r x x' → (part i).r y y' → x ≠ y → x' ≠ y' → 68 ¬ (resolved i).Adj x y → ¬ (resolved i).Adj x' y' → 69 (G.Adj x y ↔ G.Adj x' y') 70 71 namespace MergeSeq 72 73 variable {G : SimpleGraph V} 74 75 /-- The number of parts of that are **accessible** from by a 76 walk of length at most in the resolved graph . (Note the 77 intentional mismatch of indices versus .) -/ 78 noncomputable def numAccessible (S : MergeSeq G) (r i : ℕ) (v : V) : ℕ := 79 Set.ncard ((fun u => Quotient.mk (S.part (i - 1)) u) '' resolvedBall (S.resolved i) r v) 80 81 /-- The **radius- width** of a merge sequence: the maximum over all steps 82 and vertices of the number of parts of accessible from 83 within distance in . -/ 84 noncomputable def width (S : MergeSeq G) (r : ℕ) : ℕ := 85 (Finset.Icc 2 S.length).sup fun i => Finset.univ.sup fun v => S.numAccessible r i v 86 87 end MergeSeq 88 89 /-- The **radius- merge-width** of a graph : the minimum 90 radius- width over all merge sequences of . -/ 91 noncomputable def mergeWidth (r : ℕ) (G : SimpleGraph V) : ℕ := 92 sInf {w | ∃ S : MergeSeq G, S.width r = w} 93 94 /-- A **graph class**: a property of finite simple graphs. -/ 95 def GraphClass : Type 1 := ∀ ⦃V : Type⦄ [Fintype V], SimpleGraph V → Prop 96 97 /-- A class has **bounded merge-width** if there is a function such that 98 every satisfies for all radii . -/ 99 def BoundedMergeWidth (C : GraphClass) : Prop := 100 ∃ f : ℕ → ℕ, ∀ ⦃V : Type⦄ [Fintype V] (G : SimpleGraph V), C G → ∀ r, mergeWidth r G ≤ f r 101 102 end Lax9.MergeWidth 103 -
Twin-width
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.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 import Mathlib.Data.Set.Card 3 import Mathlib.Data.Nat.Lattice 4 … module docstring, 25 lines 30 31 namespace Lax228581.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 Lax228581.TwinWidth 87 -
Treewidth
A tree decomposition of a finite simple graph G consists of a finite tree T and a bag of graph vertices at each node such that every graph vertex occurs in a bag, the endpoints of every graph edge occur together in a bag, and the nodes whose bags contain any fixed vertex induce a connected subgraph of T.
The treewidth of G is the least w such that G has a tree decomposition with every bag of size at most w + 1.
1 import Mathlib.Combinatorics.SimpleGraph.Acyclic 2 import Mathlib.Data.Nat.Lattice 3 … module docstring, 21 lines 25 26 namespace Lax228581.Treewidth 27 28 /-- A tree decomposition of a simple graph: a finite tree of nodes with a bag 29 of graph vertices at each node, such that the bags cover every vertex and 30 every edge, and the nodes whose bags contain any fixed vertex induce a 31 connected subgraph of the tree. -/ 32 structure TreeDecomposition {V : Type} (G : SimpleGraph V) where 33 /-- The node type of the decomposition tree. -/ 34 Node : Type 35 /-- The decomposition tree is finite. -/ 36 [nodeFintype : Fintype Node] 37 /-- The graph on the decomposition nodes. -/ 38 tree : SimpleGraph Node 39 /-- The node graph is a tree. -/ 40 isTree : tree.IsTree 41 /-- The bag assigned to each decomposition node. -/ 42 bag : Node → Finset V 43 /-- Every graph vertex appears in at least one bag. -/ 44 vertex_mem_bag : ∀ v : V, ∃ i : Node, v ∈ bag i 45 /-- Every graph edge has both endpoints together in at least one bag. -/ 46 edge_mem_bag : ∀ ⦃u v : V⦄, G.Adj u v → ∃ i : Node, u ∈ bag i ∧ v ∈ bag i 47 /-- For each graph vertex, the nodes whose bags contain it induce a 48 connected subgraph of the tree. -/ 49 bag_indices_connected : 50 ∀ v : V, (tree.induce {i : Node | v ∈ bag i}).Connected 51 52 /-- `G` has a tree decomposition all of whose bags have at most `w + 1` 53 vertices. -/ 54 def HasTreewidthAtMost {V : Type} (G : SimpleGraph V) (w : ℕ) : Prop := 55 ∃ D : TreeDecomposition G, ∀ i, (D.bag i).card ≤ w + 1 56 57 /-- The treewidth of a finite simple graph: the least `w` such that the 58 graph has a tree decomposition with bags of at most `w + 1` vertices. -/ 59 noncomputable def treewidth {V : Type} [Fintype V] [DecidableEq V] 60 (G : SimpleGraph V) : ℕ := 61 sInf {w | HasTreewidthAtMost G w} 62 63 end Lax228581.Treewidth 64 -
Twin-width
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.
1 import Mathlib.Combinatorics.SimpleGraph.Basic 2 import Mathlib.Data.Set.Card 3 import Mathlib.Data.Nat.Lattice 4 … module docstring, 25 lines 30 31 namespace Lax228581.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 Lax228581.TwinWidth 87