Bag bounds from a graph cut

The prescribed-endpoint theorem on each side and the transition between their boundaries give the finite form of Fomin and Høie's Theorem 5.

theorem Algebraic.Cutwidth.PathDecomposition.Internal.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

theorem Algebraic.Cutwidth.PathDecomposition.Internal.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

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

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