Bounded connected partitions of subcubic graphs #
A connected subcubic graph on more than M vertices can be partitioned
into connected pieces of size at most 3 M, with at most 2 n / M
pieces. The proof recursively removes a root, partitions the resulting
components, and joins their small remainders through the root.
This supplies the bounded pieces used by the red/black density argument
in RedBlack.Clusters.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.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)
:
Partition a connected subcubic graph into disjoint connected sets of
at most 3 M vertices. Their number is at most 2 n / M, with the
positive denominator cleared.