Partial connected partitions with a rooted remainder

Removing a root splits a connected graph into at most its degree many components. Joining their small rooted remainders back to the root produces one bounded connected piece. This intermediate record supports that induction without carrying a rooted-tree representation.

structure Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Partial {V : Type} (B : SimpleGraph V) (S : Finset V) (root : V) (M : ℕ) : Type

Connected pieces of size between M and 3 M, and at most one smaller remainder containing the prescribed root.

• parts : Finset (Finset V)

  Completed connected pieces, each with at least M vertices.

• remainder : Finset V

  The still-unassigned connected set containing the root, or the empty set.

• cover : self.parts.biUnion id ∪ self.remainder = S
• disjoint : (↑self.parts).Pairwise Disjoint
• separate (P : Finset V) : P ∈ self.parts → Disjoint P self.remainder
• pieces (P : Finset V) : P ∈ self.parts → (SimpleGraph.induce {v : V | v ∈ P} B).Connected ∧ M ≤ P.card ∧ P.card ≤ 3 * M
• small : self.remainder.card < M
• rooted : self.remainder = ∅ ∨ root ∈ self.remainder ∧ (SimpleGraph.induce {v : V | v ∈ self.remainder} B).Connected