Eliminating boundary edges with a uniform reverse bound

The original boundary graph is a matching once small helpful sets have been excluded. Reversing a switch completes one of these disjoint pairs. Keep the selected boundary vertices inside their original pair closure, and charge at most two new vertices per new boundary vertex. This gives a factor-three bound for the entire sequence, independent of its length.

theorem Algebraic.Cutwidth.Bisection.BoundaryNormalization.Internal.exists_independent_boundary_or_small_helpful {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (regular : H.IsRegularOfDegree 3) : (∃ X ⊆ S, X.card ≤ 33 ∧ 1 ≤ helpfulness H S X) ∨ ∃ (G : SimpleGraph W), G.IsRegularOfDegree 3 ∧ G.cutFinset S = H.cutFinset S ∧ cutBoundary G S = cutBoundary H S ∧ (∀ c ∈ cutBoundary G S, (G.neighborFinset c \ S).card = 1) ∧ (∀ a ∈ cutBoundary G S, ∀ b ∈ cutBoundary G S, ¬G.Adj a b) ∧ ∀ X ⊆ S, ∃ Y ⊆ S, X ⊆ Y ∧ Y.card ≤ 3 * X.card ∧ helpfulness G S X ≤ helpfulness H S Y