Constructing the core forest from the region family

Disjoint connected regions with no edges between them give independent vertices in their boundary quotient. Their cuts bound their quotient degrees. If cycles avoid the regions and their cuts have size at most two, suppressing these vertices gives a forest on the remaining core pieces, with exact reachability inherited from the original graph. Its edges count exactly the regions whose remaining boundary has size two.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.Internal.exists_core_forest {V ι : Type} [Fintype V] [Fintype ι] (B : SimpleGraph V) (P : ι → Finset V) (connected : ∀ (i : ι), (SimpleGraph.induce {v : V | v ∈ P i} B).Connected) (disjoint : Pairwise fun (i j : ι) => Disjoint (P i) (P j)) (separate : ∀ (i j : ι), ∀ u ∈ P i, ∀ v ∈ P j, B.Adj u v → i = j) (boundary : ∀ (i : ι), (B.cutFinset (P i)).card ≤ 2) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) : ∃ (f : ι ↪ (B.deleteEdges (⋃ (i : ι), ↑(B.cutFinset (P i)))).ConnectedComponent), (∀ (i : ι), (f i).supp.toFinset = P i) ∧ (coreGraph B P f).IsAcyclic ∧ (coreGraph B P f).edgeSet.ncard = {i : ι | (B.cutFinset (P i)).card = 2}.card ∧ ∀ (u v : { C : (B.deleteEdges (⋃ (i : ι), ↑(B.cutFinset (P i)))).ConnectedComponent // C ∉ Finset.image (⇑f) Finset.univ }), (coreGraph B P f).Reachable u v ↔ B.Reachable (Quot.out ↑u) (Quot.out ↑v)