Invariants of the second normalization phase

The original three-boundary-neighbor vertices form the set A; P records those already processed. A processed center retains two boundary neighbors, and an unprocessed center retains all three. Every other interior vertex has at most two. In particular, the low-degree endpoint d of a later switch cannot be an original center. Each switch processes exactly one new center and preserves independence of the boundary.

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.boundaryNeighbors_switch {W : Type} [Fintype W] (G : SimpleGraph W) {C : Finset W} {a b c d : W} (valid : Switchable G a b c d) (ha : a ∉ C) (hb : b ∈ C) (hc : c ∉ C) (hd : d ∉ C) (v : W) : (switchEdges G a b c d).neighborFinset v ∩ C = if v = a then (G.neighborFinset v ∩ C).erase b else if v = d then insert b (G.neighborFinset v ∩ C) else G.neighborFinset v ∩ C

structure Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.State {W : Type} [Fintype W] (M : SimpleGraph W) (C S A : Finset W) (G : SimpleGraph W) (P : Finset W) : Prop

The current graph retains two or three original boundary neighbors at each original center, according to whether that center has been processed.

• regular : G.IsRegularOfDegree 3
• boundary : cutBoundary G S = C
• independent (a : W) : a ∈ C → ∀ b ∈ C, ¬G.Adj a b
• processed : P ⊆ A
• centers (a : W) : a ∈ A → (G.neighborFinset a ∩ C).card = if a ∈ P then 2 else 3
• original (a : W) : a ∈ A → G.neighborFinset a ∩ C ⊆ M.neighborFinset a ∩ C
• small (v : W) : v ∈ S \ C → v ∉ A → (G.neighborFinset v ∩ C).card ≤ 2

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.State.switch {W : Type} [Fintype W] {M G : SimpleGraph W} {C S A P : Finset W} {a b c d : W} (state : State M C S A G P) (inside : A ⊆ S \ C) (valid : Switchable G a b c d) (ha : a ∈ A) (fresh : a ∉ P) (hb : b ∈ C) (hc : c ∈ S \ C) (hd : d ∈ S \ C) (dSmall : (G.neighborFinset d ∩ C).card ≤ 1) : State M C S A (switchEdges G a b c d) (insert a P)