Restoring a whole family with a uniform size bound

A positive witness avoiding the isolated regions transfers back to the original graph by adding just those regions whose cuts touch the witness, together with their closed attachments. Each selected region contributes at most one new external black edge and a distinct new internal red edge. The size bound depends on the original witness, not the number of regions. Attached sets may overlap and may already be partly selected. The mark-based bound charges only the endpoint marks on the witness, at most one region-plus-attachment size per such mark. If the original set is closed in the deleted graph and contains every outside endpoint of some nonempty region boundary, restoration creates positivity: that region supplies a red edge with no remaining black cost.

For black degree at most three and region-plus-attachment size at most 4 M, the bound is (1 + 12 M) |X|. Thus an O(M) witness remains O(M²) after all paths are restored, as required in Monien and Preis's cycle-removal argument. PathSystem constructs the thin family with L = 3 M, giving the factor 1 + 9 M. Tree reorganization is not formalized; RedBlack.Clusters proves the red/black lemma by another route.

Source: Burkhard Monien and Robert Preis, Upper bounds on the bisection width of 3- and 4-regular graphs, Journal of Discrete Algorithms 4 (2006), 475–498, https://doi.org/10.1016/j.jda.2005.12.009.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.cut_deletedGraph_restrict {V E ι : Type} [Fintype V] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (cuts : Pairwise fun (i j : ι) => Disjoint (B.cutFinset (F.region i)) (B.cutFinset (F.region j))) (indices : Finset ι) (i : ι) : (F.restrict indices).deletedGraph.cutFinset (F.region i) = if i ∈ indices then ∅ else B.cutFinset (F.region i)

For pairwise disjoint region cuts, isolating a subfamily empties exactly its cuts and preserves the cuts of all other regions.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.exists_positive_of_closed_core {V E ι : Type} [Fintype V] [Fintype E] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (L : ℕ) (small : ∀ (i : ι), (F.region i ∪ F.attachment i).card ≤ L) {X : Finset V} (fresh : ∀ (i : ι), Disjoint X (F.region i)) (closed : F.deletedGraph.cutFinset X = ∅) {i : ι} (nonempty : (B.cutFinset (F.region i)).Nonempty) (absorbed : B.cutFinset (F.region i) ⊆ B.cutFinset X) : ∃ (Y : Finset V), X ⊆ Y ∧ Y.card ≤ X.card + L * (B.cutFinset X).card ∧ Positive B R Y

A closed set of core vertices becomes positive after restoring the incident regions if it absorbs the entire nonempty boundary of one region.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.exists_positive_of_closed_core_of_degree {V E ι : Type} [Fintype V] [Fintype E] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (L d : ℕ) (small : ∀ (i : ι), (F.region i ∪ F.attachment i).card ≤ L) {X : Finset V} (fresh : ∀ (i : ι), Disjoint X (F.region i)) (closed : F.deletedGraph.cutFinset X = ∅) (degree : ∀ v ∈ X, B.degree v ≤ d) {i : ι} (nonempty : (B.cutFinset (F.region i)).Nonempty) (absorbed : B.cutFinset (F.region i) ⊆ B.cutFinset X) : ∃ (Y : Finset V), X ⊆ Y ∧ Y.card ≤ (1 + d * L) * X.card ∧ Positive B R Y

In bounded degree, a closed core set absorbing one complete region boundary gives a positive witness whose size is linear in the core size.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.exists_positive_restore {V E ι : Type} [Fintype V] [Fintype E] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (L : ℕ) (small : ∀ (i : ι), (F.region i ∪ F.attachment i).card ≤ L) {X : Finset V} (fresh : ∀ (i : ι), Disjoint X (F.region i)) (positive : Positive F.deletedGraph R X) : ∃ (Y : Finset V), X ⊆ Y ∧ Y.card ≤ X.card + L * (B.cutFinset X).card ∧ Positive B R Y

Restore all deleted cuts. At most one region and its attachment need be added per black edge crossing the original witness.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.exists_positive_restore_by_marks {V E ι : Type} [Fintype V] [Fintype E] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (L : ℕ) (small : ∀ (i : ι), (F.region i ∪ F.attachment i).card ≤ L) {X : Finset V} (fresh : ∀ (i : ι), Disjoint X (F.region i)) (positive : Positive F.deletedGraph R X) : ∃ (Y : Finset V), X ⊆ Y ∧ Y.card ≤ X.card + L * ∑ v ∈ X, F.endpointMarks v ∧ Positive B R Y

Restore the witness by paying at most L added vertices per endpoint mark on the witness. Only marks on the original witness enter the size bound.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.exists_positive_restore_of_degree {V E ι : Type} [Fintype V] [Fintype E] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) (L d : ℕ) (small : ∀ (i : ι), (F.region i ∪ F.attachment i).card ≤ L) {X : Finset V} (fresh : ∀ (i : ι), Disjoint X (F.region i)) (degree : ∀ v ∈ X, B.degree v ≤ d) (positive : Positive F.deletedGraph R X) : ∃ (Y : Finset V), X ⊆ Y ∧ Y.card ≤ (1 + d * L) * X.card ∧ Positive B R Y

Bounded degree turns simultaneous restoration into a size bound that is independent of the total number of deleted regions.