Eliminating three-boundary-neighbor vertices

After excluding small helpful sets, the original three-neighbor stars are disjoint. Each switch processes a fresh center. In reverse order, the potential from Potential pays for all extensions. Its initial value is at most five times the selected set's size, and its final value is the size of the transferred set. This supplies the uniform reverse bound for the second phase of Monien and Preis's normalization argument.

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.exists_no_three_neighbors_or_small_helpful {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (regular : H.IsRegularOfDegree 3) (independent : ∀ a ∈ cutBoundary H S, ∀ b ∈ cutBoundary H S, ¬H.Adj a b) : (∃ X ⊆ S, X.card ≤ 55 ∧ 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) ∧ (∀ v ∈ S \ cutBoundary G S, (G.neighborFinset v ∩ cutBoundary G S).card ≤ 2) ∧ ∀ X ⊆ S, ∃ Y ⊆ S, X ⊆ Y ∧ Y.card ≤ 5 * X.card ∧ helpfulness G S X ≤ helpfulness H S Y

theorem Algebraic.Cutwidth.Bisection.NeighborNormalization.Internal.exists_normalization_or_small_helpful {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (regular : H.IsRegularOfDegree 3) : (∃ X ⊆ S, X.card ≤ 165 ∧ 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) ∧ (∀ v ∈ S \ cutBoundary G S, (G.neighborFinset v ∩ cutBoundary G S).card ≤ 2) ∧ ∀ X ⊆ S, ∃ Y ⊆ S, X ⊆ Y ∧ Y.card ≤ 15 * X.card ∧ helpfulness G S X ≤ helpfulness H S Y