The core forest after path suppression

Connected, disjoint regions separated from one another give distinct independent vertices in the boundary quotient. When their cuts have size at most two and cycles avoid them, suppressing these region vertices produces a forest on the remaining core pieces, with exactly the original reachability between those pieces. The number of core edges is exactly the number of regions with two boundary edges.

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

Construct the forest on the pieces outside all regions, suppressing the region vertices and preserving reachability between representative vertices. Its edges count exactly the regions with two boundary edges.