Path decompositions and the pathwidth hypothesis

A path decomposition of a simple graph is a sequence of bags covering every vertex and every edge, in which the bags containing a fixed vertex are consecutive. Its width is one less than the largest bag.

PathwidthBound ξ N₀ is the pathwidth theorem for cubic graphs, taken as a hypothesis: every simple 3-regular graph on more than N₀ vertices has a path decomposition of width at most (1/6 + ξ) h, where h is the number of vertices. Together with the compression and median-ordering arguments it yields the graph-ordering hypothesis Multigraph.OrderingBound.

The cut of a vertex set in a simple graph, SimpleGraph.cutFinset, is the set of edges with exactly one endpoint in the set.

structure Algebraic.Cutwidth.PathDecomposition {W : Type} (H : SimpleGraph W) : Type

A path decomposition: bags indexed by Fin length, covering every vertex and every edge, with the bags containing any vertex forming an interval.

• length : ℕ

  The number of bags.

• bag : Fin self.length → Finset W

  The bags.

• vertex_mem (w : W) : ∃ (i : Fin self.length), w ∈ self.bag i

  Every vertex lies in some bag.

• edge_mem (u v : W) : H.Adj u v → ∃ (i : Fin self.length), u ∈ self.bag i ∧ v ∈ self.bag i

  Both endpoints of every edge lie in a common bag.

• consecutive (w : W) (i j k : Fin self.length) : i ≤ j → j ≤ k → w ∈ self.bag i → w ∈ self.bag k → w ∈ self.bag j

  The bags containing a vertex are consecutive.

def Algebraic.Cutwidth.PathDecomposition.trivial {W : Type} (H : SimpleGraph W) [Fintype W] : PathDecomposition H

The one-bag decomposition of a finite graph.

Equations

• Algebraic.Cutwidth.PathDecomposition.trivial H = { length := 1, bag := fun (x : Fin 1) => Finset.univ, vertex_mem := ⋯, edge_mem := ⋯, consecutive := ⋯ }

def Algebraic.Cutwidth.PathwidthBound (ξ : ℝ) (N₀ : ℕ) : Prop

The pathwidth hypothesis for cubic graphs with slack ξ and threshold N₀: every simple 3-regular graph on h > N₀ vertices has a path decomposition all of whose bags have at most (1/6 + ξ) h + 1 vertices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SimpleGraph.cutFinset {W : Type} (H : SimpleGraph W) [Fintype W] (S : Finset W) : Finset (Sym2 W)

The edges of a simple graph with exactly one endpoint in S.

Equations

• H.cutFinset S = {e ∈ H.edgeFinset | ∃ (a : W) (b : W), e = s(a, b) ∧ a ∈ S ∧ b ∉ S}

theorem SimpleGraph.mem_cutFinset {W : Type} (H : SimpleGraph W) [Fintype W] {S : Finset W} {e : Sym2 W} : e ∈ H.cutFinset S ↔ e ∈ H.edgeSet ∧ ∃ (a : W) (b : W), e = s(a, b) ∧ a ∈ S ∧ b ∉ S

theorem SimpleGraph.mem_cutFinset_mk {W : Type} (H : SimpleGraph W) [Fintype W] {S : Finset W} {a b : W} : s(a, b) ∈ H.cutFinset S ↔ H.Adj a b ∧ (a ∈ S ∧ b ∉ S ∨ b ∈ S ∧ a ∉ S)

An edge crossing a set is adjacent-pair witnessed with the inside endpoint first.

theorem SimpleGraph.cutFinset_eq_empty_of_subsingleton {W : Type} (H : SimpleGraph W) [Fintype W] [Subsingleton W] (S : Finset W) : H.cutFinset S = ∅

A graph with at most one vertex has no crossing edges.