Logarithmic-width decompositions of trees

Repeatedly deleting a centroid gives bags of size at most ⌈log₂ n⌉ + 1. This elementary bound suffices for the tree component in Fomin and Høie's endpoint induction; their sharper logarithmic term is not needed for the asymptotic coefficient 1/6 in the cubic-graph pathwidth bound.

theorem Algebraic.Cutwidth.exists_tree_centroid {W : Type} [Fintype W] {H : SimpleGraph W} (tree : H.IsTree) : ∃ (r : W), ∀ (C : (SimpleGraph.induce {w : W | w ≠ r} H).ConnectedComponent), 2 * Fintype.card ↥C ≤ Fintype.card W

A finite tree has a vertex whose deletion leaves components of size at most half the original tree.

theorem Algebraic.Cutwidth.PathDecomposition.exists_tree_of_card_le_pow {W : Type} [Fintype W] {H : SimpleGraph W} (tree : H.IsTree) {k : ℕ} (hcard : Fintype.card W ≤ 2 ^ k) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ k + 1

Trees with at most 2 ^ k vertices admit bags of size at most k + 1.

theorem Algebraic.Cutwidth.PathDecomposition.exists_tree {W : Type} [Fintype W] {H : SimpleGraph W} (tree : H.IsTree) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ Nat.clog 2 (Fintype.card W) + 1

A finite tree has pathwidth at most the ceiling of its base-two logarithm.

theorem Algebraic.Cutwidth.PathDecomposition.exists_forest {W : Type} [Fintype W] {H : SimpleGraph W} (forest : H.IsAcyclic) : ∃ (D : PathDecomposition H), ∀ (i : Fin D.length), (D.bag i).card ≤ Nat.clog 2 (Fintype.card W) + 1

The logarithmic tree bound extends to every finite acyclic graph.