Constructing the degree-two regions

Induced connected components partition the eligible vertices, with no black edges between distinct regions. Their boundary cuts are therefore pairwise disjoint. Degree at most two gives a spanning path and at most two boundary edges; degree exactly two makes the boundary size even.

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.mem_region {V : Type} (B : SimpleGraph V) (U : Finset V) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) {v : V} : v ∈ region B U C ↔ ∃ (h : v ∈ U), ⟨v, h⟩ ∈ C.supp

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.region_subset {V : Type} (B : SimpleGraph V) (U : Finset V) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) : region B U C ⊆ U

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.region_connected {V : Type} (B : SimpleGraph V) (U : Finset V) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) : (SimpleGraph.induce {v : V | v ∈ region B U C} B).Connected

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_mem_region {V : Type} (B : SimpleGraph V) (U : Finset V) {v : V} : (∃ (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent), v ∈ region B U C) ↔ v ∈ U

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.region_disjoint {V : Type} (B : SimpleGraph V) (U : Finset V) : Pairwise fun (C D : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) => Disjoint (region B U C) (region B U D)

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.eq_of_adj {V : Type} (B : SimpleGraph V) (U : Finset V) {C D : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent} {v w : V} (hv : v ∈ region B U C) (hw : w ∈ region B U D) (adjacent : B.Adj v w) : C = D

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.cut_disjoint {V : Type} (B : SimpleGraph V) (U : Finset V) [Fintype V] : Pairwise fun (C D : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) => Disjoint (B.cutFinset (region B U C)) (B.cutFinset (region B U D))

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.exists_distinct_boundary_edges {V : Type} (B : SimpleGraph V) (U : Finset V) [Fintype V] (components : Finset (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) (boundary : ∀ C ∈ components, (B.cutFinset (region B U C)).Nonempty) : ∃ (chosen : ↥components → Sym2 V), Function.Injective chosen ∧ ∀ (C : ↥components), chosen C ∈ B.cutFinset (region B U ↑C)

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.region_spanning_path {V : Type} (B : SimpleGraph V) (U : Finset V) [Fintype V] (degree : ∀ v ∈ U, B.degree v ≤ 2) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) : ∃ (u : V) (v : V) (p : B.Walk u v), p.IsPath ∧ p.support.toFinset = region B U C

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.card_cut_le_two {V : Type} (B : SimpleGraph V) (U : Finset V) [Fintype V] (degree : ∀ v ∈ U, B.degree v ≤ 2) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) : (B.cutFinset (region B U C)).card ≤ 2

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.card_cut_eq_zero_or_two {V : Type} (B : SimpleGraph V) (U : Finset V) [Fintype V] (degree : ∀ v ∈ U, B.degree v = 2) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) : (B.cutFinset (region B U C)).card = 0 ∨ (B.cutFinset (region B U C)).card = 2

theorem Algebraic.Cutwidth.Bisection.RedBlack.PathSystem.Internal.region_isTree {V : Type} (B : SimpleGraph V) (U : Finset V) [Fintype V] (degree : ∀ v ∈ U, B.degree v ≤ 2) (C : (SimpleGraph.induce {v : V | v ∈ U} B).ConnectedComponent) (boundary : (B.cutFinset (region B U C)).Nonempty) : (SimpleGraph.induce {v : V | v ∈ region B U C} B).IsTree