Bounded connected partitions of subcubic graphs

Induction on the vertex set partitions each connected region into pieces of size between M and 3 M, with at most one smaller rooted remainder. There are at most three components after removing a root, so joining their remainders stays within the size bound. Adding the final remainder gives at most 2 n / M pieces whenever n > M.

theorem Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Internal.exists_partial {V : Type} [Fintype V] (B : SimpleGraph V) (degree : ∀ (v : V), B.degree v ≤ 3) (M : ℕ) (positive : 0 < M) (S : Finset V) (root : V) (member : root ∈ S) (connected : (SimpleGraph.induce {v : V | v ∈ S} B).Connected) : Nonempty (Partial B S root M)

theorem Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Internal.exists_partition {V : Type} [Fintype V] (B : SimpleGraph V) (connected : B.Connected) (degree : ∀ (v : V), B.degree v ≤ 3) (M : ℕ) (positive : 0 < M) (large : M < Fintype.card V) : ∃ (parts : Finset (Finset V)), parts.biUnion id = Finset.univ ∧ (↑parts).Pairwise Disjoint ∧ (∀ P ∈ parts, (SimpleGraph.induce {v : V | v ∈ P} B).Connected ∧ P.card ≤ 3 * M) ∧ M * parts.card ≤ 2 * Fintype.card V