The core forest for the constructed thin paths

Isolating a selected thin region deletes no internal edge of any region. The regions therefore remain connected and separated, and their remaining cuts have size at most two. Identify and suppress their quotient vertices to obtain the forest on the core pieces. Its reachability agrees with the original black graph, since core representatives avoid every thin region. If eligible vertices have degree exactly two, every original thin boundary has size two. Isolation empties precisely the shaded cuts, so the core edges count the unshaded thin paths exactly.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_core_forest {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)) (shaded : Finset ↥(thinComponents B R U M)), have H := (F.restrict shaded).deletedGraph; ∃ (f : ↥(thinComponents B R U M) ↪ (H.deleteEdges (⋃ (i : ↥(thinComponents B R U M)), ↑(H.cutFinset (F.region i)))).ConnectedComponent), (∀ (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) ∧ shaded.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent ∧ SmallCycleBudget B M shaded.card ∧ (∀ (C : ↥(thinComponents B R U M)), (f C).supp.toFinset = F.region C) ∧ (PathSuppression.coreGraph H F.region f).IsAcyclic ∧ (PathSuppression.coreGraph H F.region f).edgeSet.ncard = {C : ↥(thinComponents B R U M) | (H.cutFinset (F.region C)).card = 2}.card ∧ ∀ (u v : { C : (H.deleteEdges (⋃ (i : ↥(thinComponents B R U M)), ↑(H.cutFinset (F.region i)))).ConnectedComponent // C ∉ Finset.image (⇑f) Finset.univ }), (PathSuppression.coreGraph H F.region f).Reachable u v ↔ B.Reachable (Quot.out ↑u) (Quot.out ↑v)

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_counted_core_forest {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)) (shaded : Finset ↥(thinComponents B R U M)), have H := (F.restrict shaded).deletedGraph; ∃ (f : ↥(thinComponents B R U M) ↪ (H.deleteEdges (⋃ (i : ↥(thinComponents B R U M)), ↑(H.cutFinset (F.region i)))).ConnectedComponent), (∀ (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) ∧ shaded.card + Fintype.card V ≤ B.edgeFinset.card + Nat.card B.ConnectedComponent ∧ SmallCycleBudget B M shaded.card ∧ (∀ (C : ↥(thinComponents B R U M)), (f C).supp.toFinset = F.region C) ∧ (PathSuppression.coreGraph H F.region f).IsAcyclic ∧ (PathSuppression.coreGraph H F.region f).edgeSet.ncard + shaded.card = (thinComponents B R U M).card ∧ ∀ (u v : { C : (H.deleteEdges (⋃ (i : ↥(thinComponents B R U M)), ↑(H.cutFinset (F.region i)))).ConnectedComponent // C ∉ Finset.image (⇑f) Finset.univ }), (PathSuppression.coreGraph H F.region f).Reachable u v ↔ B.Reachable (Quot.out ↑u) (Quot.out ↑v)