Constructing the thin-path restoration family

Select the induced degree-two regions that are thin relative to their actual red attachments to small black components. Unless a positive set of at most 8 M + 1 vertices already exists, each selected region has one or two attachments, at most 2 M vertices, and a nonempty black boundary. Choose one attached small component per region. When eligible vertices belong to large black components, this constructs a restoration family whose region plus attachment has at most 3 M vertices.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.mem_attachmentEdges {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {P : Finset V} {M : ℕ} {e : E} : e ∈ attachmentEdges B R P M ↔ R.fst e ∈ P ∧ Fintype.card ↥(B.connectedComponentMk (R.snd e)) ≤ M ∨ R.snd e ∈ P ∧ Fintype.card ↥(B.connectedComponentMk (R.fst e)) ≤ M

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.attachment_spec {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {P : Finset V} {M : ℕ} {e : E} (member : e ∈ attachmentEdges B R P M) : B.cutFinset (attachment B R P M e) = ∅ ∧ (attachment B R P M e).card ≤ M ∧ (R.fst e ∈ P ∧ R.snd e ∈ attachment B R P M e ∨ R.snd e ∈ P ∧ R.fst e ∈ attachment B R P M e)

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.attachment_disjoint {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {P U : Finset V} {M : ℕ} {e : E} (large : ∀ v ∈ U, M < Fintype.card ↥(B.connectedComponentMk v)) (member : e ∈ attachmentEdges B R P M) : Disjoint U (attachment B R P M e)

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.attachmentComponent_card_le {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {P : Finset V} {M : ℕ} {e : E} (member : e ∈ attachmentEdges B R P M) : Fintype.card ↥(attachmentComponent B R P M e) ≤ M

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.mem_thinComponents {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) {U : Finset V} {M : ℕ} {C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent} : C ∈ thinComponents B R U M ↔ (region B U C).card ≤ M * (attachmentEdges B R (region B U C) M).card

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.thin_component_bounds {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (degree : ∀ v ∈ U, B.degree v ≤ 2) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) {C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent} (thin : C ∈ thinComponents B R U M) : (attachmentEdges B R (region B U C) M).Nonempty ∧ (attachmentEdges B R (region B U C) M).card ≤ 2 ∧ (region B U C).card ≤ 2 * M ∧ (B.cutFinset (region B U C)).Nonempty

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.card_cut_thin_eq_two {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (degree : ∀ v ∈ U, B.degree v = 2) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) {C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent} (thin : C ∈ thinComponents B R U M) : (B.cutFinset (region B U C)).card = 2

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_restorationFamily {V E : Type} [Fintype V] [Fintype E] (B : SimpleGraph V) (R : Multigraph V E) (U : Finset V) (M : ℕ) (degree : ∀ v ∈ U, B.degree v ≤ 2) (large : ∀ v ∈ U, M < Fintype.card ↥(B.connectedComponentMk v)) (noPositive : ¬∃ (X : Finset V), X.card ≤ 8 * M + 1 ∧ Positive B R X) : ∃ (F : RestorationFamily B R ↥(thinComponents B R U M)), (∀ (C : ↥(thinComponents B R U M)), F.region C = region B U ↑C) ∧ (∀ (C : ↥(thinComponents B R U M)), (F.region C ∪ F.attachment C).card ≤ 3 * M) ∧ ∀ (C : ↥(thinComponents B R U M)), (B.cutFinset (F.region C)).Nonempty