Simultaneous restoration of isolated regions

Add exactly the regions whose black cuts meet the original witness's cut, together with their closed attachments. Each such region leaves at most one new external black edge and supplies a distinct new internal red edge. No other deleted edge can cross the enlarged witness. The number of added regions is at most the size of the original black cut.

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.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)

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.exists_positive_of_closed_core {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) [Fintype E] (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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.exists_positive_of_closed_core_of_degree {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) [Fintype E] (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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.exists_positive_restore {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) [Fintype E] (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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.exists_positive_restore_by_marks {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) [Fintype E] (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

theorem Algebraic.Cutwidth.Bisection.RedBlack.RestorationFamily.Internal.exists_positive_restore_of_degree {V E ι : Type} [Fintype V] [Fintype ι] {B : SimpleGraph V} {R : Multigraph V E} (F : RestorationFamily B R ι) [Fintype E] (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