Connectivity outside the isolated regions #
After deleting one boundary edge of a region with at most two boundary edges, its remaining boundary has size at most one. A simple path between vertices outside that region cannot enter it and leave again: that would repeat its sole boundary edge. Deleting the remaining boundary therefore preserves reachability between outside vertices. This works for a whole family simultaneously and supplies the core-connectivity invariant in Monien and Preis's cycle-removal step.
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.trail_avoids_cut_of_card_le_one
{V : Type}
[Fintype V]
(B : SimpleGraph V)
{P : Finset V}
(one : (B.cutFinset P).card ≤ 1)
{u v : V}
{p : B.Walk u v}
(trail : p.IsTrail)
(hu : u ∉ P)
(hv : v ∉ P)
{e : Sym2 V}
(boundary : e ∈ B.cutFinset P)
:
e ∉ p.edges
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.cut_card_le_one_after_chosen_deletion
{V : Type}
[Fintype V]
(B : SimpleGraph V)
{ι : Type}
(P : ι → Finset V)
(chosen : ι → Sym2 V)
(indices : Finset ι)
(two : ∀ i ∈ indices, (B.cutFinset (P i)).card ≤ 2)
(boundary : ∀ i ∈ indices, chosen i ∈ B.cutFinset (P i))
{i : ι}
(hi : i ∈ indices)
:
theorem
Algebraic.Cutwidth.Bisection.RedBlack.CycleRemoval.Internal.reachable_after_isolating
{V : Type}
[Fintype V]
(B : SimpleGraph V)
{ι : Type}
(P : ι → Finset V)
(chosen : ι → Sym2 V)
(indices : Finset ι)
(two : ∀ i ∈ indices, (B.cutFinset (P i)).card ≤ 2)
(boundary : ∀ i ∈ indices, chosen i ∈ B.cutFinset (P i))
(preserved : (B.deleteEdges ↑(Finset.image chosen indices)).Reachable = B.Reachable)
{u v : V}
(hu : ∀ i ∈ indices, u ∉ P i)
(hv : ∀ i ∈ indices, v ∉ P i)
: