The sharp bisection bound from bounded helpful sets

The global argument follows Monien and Preis's local-improvement scheme, using the proved endpoint-based rebalancing bound. Its maximum with the side size handles overshoot without a separate correction of the helpful move. Only the bounded local helpful-set lemma remains an input.

theorem Algebraic.Cutwidth.Bisection.Internal.exists_bisection_of_helpful {W : Type} [Fintype W] (H : SimpleGraph W) (regular : H.IsRegularOfDegree 3) {ξ : ℝ} (hξ : 0 < ξ) (M : ℕ) (budget : (↑M + 3) * (↑(Nat.clog 2 (Fintype.card W)) + 4) < ξ * ↑(Fintype.card W)) (find : ∀ (S : Finset W), (1 / 3 + ξ) * ↑S.card < ↑(H.cutFinset S).card → ∃ X ⊆ S, X.card ≤ M ∧ 1 ≤ helpfulness H S X) : ∃ (S : Finset W), S.card ≤ Sᶜ.card + 1 ∧ Sᶜ.card ≤ S.card + 1 ∧ ↑(H.cutFinset S).card ≤ (1 / 6 + ξ) * ↑(Fintype.card W)

theorem Algebraic.Cutwidth.Bisection.Internal.exists_bisectionBound_of_helpful {ξ : ℝ} (hξ : 0 < ξ) (M : ℕ) (find : ∀ (W : Type) [inst : Fintype W] [DecidableEq W] (H : SimpleGraph W) [inst_2 : DecidableRel H.Adj], H.IsRegularOfDegree 3 → ∀ (S : Finset W), (1 / 3 + ξ) * ↑S.card < ↑(H.cutFinset S).card → ∃ X ⊆ S, X.card ≤ M ∧ 1 ≤ helpfulness H S X) : ∃ (N₀ : ℕ), BisectionBound ξ N₀