Contracting the pieces between bridges

The component quotient preserves reachability. If every designated edge is a bridge, it is a forest, and every one of its connected components is a tree. The quotient also preserves the designated actual edges exactly: none becomes a loop and distinct edges do not merge into parallel copies.

In Monien and Preis's red/black argument, cycles avoid all thin regions after cycle removal. Every surviving region-boundary edge is therefore a bridge, so contracting the pieces between those boundaries gives a forest. This supplies the contraction step. PathSuppression removes the thin-path vertices from the quotient. The weighted-tree reorganization is not formalized; RedBlack.Clusters proves the red/black lemma by another route.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.reachable_project {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) {u v : V} (reachable : B.Reachable u v) : (graph B F).Reachable ((B.deleteEdges F).connectedComponentMk u) ((B.deleteEdges F).connectedComponentMk v)

Original walks project to reachability between the corresponding quotient vertices.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.reachable_iff {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) {C D : (B.deleteEdges F).ConnectedComponent} {u v : V} (hu : u ∈ C.supp) (hv : v ∈ D.supp) : (graph B F).Reachable C D ↔ B.Reachable u v

Quotient reachability is exactly original reachability between any chosen representatives.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.connected {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (original : B.Connected) : (graph B F).Connected

Contracting connected pieces preserves connectedness.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.edge_image {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : Sym2.map (B.deleteEdges F).connectedComponentMk '' (F ∩ B.edgeSet) = (graph B F).edgeSet

The designated actual edges map onto all quotient edges, without loops.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.edge_map_injOn {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : Set.InjOn (Sym2.map (B.deleteEdges F).connectedComponentMk) (F ∩ B.edgeSet)

Distinct designated bridges remain distinct edges after contraction.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.edge_ncard {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : (graph B F).edgeSet.ncard = (F ∩ B.edgeSet).ncard

The quotient has exactly as many edges as there are designated actual bridges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.isAcyclic {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : (graph B F).IsAcyclic

Contracting the connected pieces between bridges produces a forest.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.isTree {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (original : B.Connected) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) : (graph B F).IsTree

A connected graph gives a tree when the contracted pieces are separated by bridges.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.component_isTree {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) (C : (graph B F).ConnectedComponent) : C.toSimpleGraph.IsTree

Each component of a bridge quotient is a tree, including isolated vertices.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.induce_delete_region_cuts {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (disjoint : Pairwise fun (i j : ι) => Disjoint (P i) (P j)) (removed : Set (Sym2 V)) (subset : removed ⊆ ⋃ (i : ι), ↑(B.cutFinset (P i))) (i : ι) : SimpleGraph.induce {v : V | v ∈ P i} (B.deleteEdges removed) = SimpleGraph.induce {v : V | v ∈ P i} B

Deleting region boundaries preserves the induced graph inside each disjoint region.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.exists_region_embedding {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (connected : ∀ (i : ι), (SimpleGraph.induce {v : V | v ∈ P i} B).Connected) (disjoint : Pairwise fun (i j : ι) => Disjoint (P i) (P j)) : ∃ (f : ι ↪ (B.deleteEdges (⋃ (j : ι), ↑(B.cutFinset (P j)))).ConnectedComponent), ∀ (i : ι), (f i).supp.toFinset = P i

Disjoint connected regions are distinct vertices of the region-boundary quotient, with exactly their original supports.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.ncard_neighborSet_le_cut {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) [Fintype V] (C : (B.deleteEdges F).ConnectedComponent) : ((graph B F).neighborSet C).ncard ≤ (B.cutFinset C.supp.toFinset).card

Each quotient neighbor requires a distinct edge of the original component's boundary.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.ncard_neighborSet_eq_cut {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) [Fintype V] (bridges : ∀ e ∈ F ∩ B.edgeSet, B.IsBridge e) (C : (B.deleteEdges F).ConnectedComponent) : ((graph B F).neighborSet C).ncard = (B.cutFinset C.supp.toFinset).card

For a bridge quotient, boundary edges correspond to distinct neighbors, so contraction preserves each component's boundary degree exactly.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.isBridge_of_mem_region_cut {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) {i : ι} {e : Sym2 V} (member : e ∈ B.cutFinset (P i)) : B.IsBridge e

A region-boundary edge is a bridge whenever all cycles avoid the regions.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.ofRegions_isAcyclic {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) : (ofRegions B P).IsAcyclic

If every cycle avoids the regions, contracting the pieces between their boundaries produces a forest.

theorem Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.ofRegions_component_isTree {V : Type} (B : SimpleGraph V) [Fintype V] {ι : Type} (P : ι → Finset V) (avoids : ∀ (u : V) (p : B.Walk u u), p.IsCycle → ∀ (i : ι), ∀ v ∈ P i, v ∉ p.support) (C : (ofRegions B P).ConnectedComponent) : C.toSimpleGraph.IsTree

After cycles through the regions have been eliminated, every component of the region-boundary quotient is a tree.