Cycle selection for the constructed thin-path system

Construct the thin regions and their compensating small components, choose distinct boundary edges using disjointness of the cuts, and apply cycle selection. The result records both the reachability-preserving single-edge deletions and the full-cut deletions used to isolate the selected paths.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_isolated_family {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)) (chosen : ↥(thinComponents B R U M) → Sym2 V) (shaded : Finset ↥(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)), chosen C ∈ B.cutFinset (F.region C)) ∧ Function.Injective chosen ∧ shaded.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent ∧ SmallCycleBudget B M shaded.card ∧ (B.deleteEdges ↑(Finset.image chosen shaded)).Reachable = B.Reachable ∧ (∀ (u v : V), (∀ C ∈ shaded, u ∉ F.region C) → (∀ C ∈ shaded, v ∉ F.region C) → ((F.restrict shaded).deletedGraph.Reachable u v ↔ B.Reachable u v)) ∧ (BridgeQuotient.ofRegions (F.restrict shaded).deletedGraph F.region).IsAcyclic ∧ ∀ (u : V) (p : (F.restrict shaded).deletedGraph.Walk u u), p.IsCycle → ∀ (C : ↥(thinComponents B R U M)), ∀ v ∈ F.region C, v ∉ p.support