Prescribed endpoints in subcubic graphs

The endpoint induction of Fomin and Høie's Pathwidth of cubic graphs and exact algorithms (2006), Lemma 4, using the elementary base-two tree bound. This finite result has no bisection hypothesis. Bisection uses it to prove the cubic pathwidth theorem from the Monien–Preis bisection hypothesis.

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

Every finite graph of maximum degree three has a decomposition ending at any prescribed set X, with the stated bag-size bound. The base-two logarithmic remainder suffices for the asymptotic cubic pathwidth theorem.