The subcubic endpoint induction

This proves the prescribed-endpoint decomposition in Fomin and Høie's Lemma 4, using the elementary base-two tree bound. The resulting bags have size at most max |X| (n / 3 + 1) + ceil(log₂ n) + 1.

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