Pathwidth from a cubic bisection bound

This completes the reduction in Fomin and Høie's Pathwidth of cubic graphs and exact algorithms (2006), Theorem 5. For any cut of a subcubic graph, the decompositions of its sides and their boundary graph concatenate with the explicit finite bound below. For balanced cuts, every positive linear slack absorbs the logarithmic remainder.

Bisection.Helpful proves the Monien–Preis theorem asserting BisectionBound ξ N₀ for every positive ξ and some N₀, then applies this reduction to obtain the sharp pathwidth bound.

theorem Algebraic.Cutwidth.PathDecomposition.exists_of_cut {W : Type} [Fintype W] (H : SimpleGraph W) (degree : ∀ (v : W), H.degree v ≤ 3) (S : Finset W) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ max (H.cutFinset S).card (max S.card Sᶜ.card / 3 + 1) + Nat.clog 2 (Fintype.card W) + 1

Decompose both sides of any cut and join them through their boundaries. This bound requires only maximum degree three, with no bisection hypothesis.

theorem Algebraic.Cutwidth.PathDecomposition.exists_of_balanced_cut {W : Type} [Fintype W] (H : SimpleGraph W) (degree : ∀ (v : W), H.degree v ≤ 3) (S : Finset W) (leftSmall : S.card ≤ Sᶜ.card + 1) (rightSmall : Sᶜ.card ≤ S.card + 1) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ max (H.cutFinset S).card ((Fintype.card W + 1) / 6 + 1) + Nat.clog 2 (Fintype.card W) + 1

For a balanced cut, each side contributes at most one sixth of the total vertex count, rounded as indicated, plus the logarithmic remainder.

theorem Algebraic.Cutwidth.bisectionBound_coarse : BisectionBound (4 / 3) 0

Every cubic graph admits a balanced cut of size at most 3n/2, simply because this counts all its edges. This coarse instance is unconditional.

theorem Algebraic.Cutwidth.BisectionBound.mono {ξ ξ' : ℝ} {N₀ N₁ : ℕ} (h : BisectionBound ξ N₀) (hξ : ξ ≤ ξ') (hN : N₀ ≤ N₁) : BisectionBound ξ' N₁

Increasing the slack and the size threshold weakens the bisection bound.

theorem Algebraic.Cutwidth.BisectionBound.exists_pathwidthBound {ξ δ : ℝ} {N₀ : ℕ} (bisection : BisectionBound ξ N₀) (hξ : 0 ≤ ξ) (hδ : 0 < δ) : ∃ (N₁ : ℕ), PathwidthBound (1 / 6) (ξ + δ) N₁

Every positive additional slack absorbs the finite decomposition's logarithmic remainder. The bisection theorem is the only graph hypothesis.

theorem Algebraic.Cutwidth.pathwidthBound_of_bisectionBound (bisection : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), BisectionBound ξ N₀) (ξ : ℝ) : 0 < ξ → ∃ (N₁ : ℕ), PathwidthBound (1 / 6) ξ N₁

The sharp asymptotic bisection theorem implies the sharp asymptotic cubic pathwidth theorem. Half the slack pays for the logarithmic remainder.