Uniformly bounded helpful sets and sharp cubic bisections

The finite red-density theorem supplies a positive set in every normalized side whose cut density exceeds 1/3 by a fixed positive amount. Suppression lifts it with a factor four, and reversing boundary normalization costs a factor three. The uniform helpful-set bound then gives the asymptotic cubic bisection theorem through the existing accumulation and rebalancing reduction.

Source: Burkhard Monien and Robert Preis, Upper bounds on the bisection width of 3- and 4-regular graphs, Journal of Discrete Algorithms 4 (2006), 475–498, https://doi.org/10.1016/j.jda.2005.12.009.

theorem Algebraic.Cutwidth.Bisection.Internal.exists_normalized_helpful_of_density {W : Type} [Fintype W] (H : SimpleGraph W) {S : Finset W} (regular : H.IsRegularOfDegree 3) (outside : ∀ c ∈ cutBoundary H S, (H.neighborFinset c \ S).card = 1) (independent : ∀ c ∈ cutBoundary H S, ∀ d ∈ cutBoundary H S, ¬H.Adj c d) {ξ : ℝ} (hξ : 0 < ξ) (M : ℕ) (positive : 0 < M) (budget : 4 ≤ 3 * ξ * ↑M) (dense : (1 / 3 + ξ) * ↑S.card < ↑(H.cutFinset S).card) : ∃ X ⊆ S, X.card ≤ 12 * M * (1 + 3 * M) ∧ 1 ≤ helpfulness H S X

theorem Algebraic.Cutwidth.Bisection.Internal.exists_bounded_helpful {W : Type} [Fintype W] (H : SimpleGraph W) (regular : H.IsRegularOfDegree 3) {ξ : ℝ} (hξ : 0 < ξ) (M : ℕ) (positive : 0 < M) (budget : 4 ≤ 3 * ξ * ↑M) {S : Finset W} (dense : (1 / 3 + ξ) * ↑S.card < ↑(H.cutFinset S).card) : ∃ X ⊆ S, X.card ≤ 36 * M * (1 + 3 * M) ∧ 1 ≤ helpfulness H S X

theorem Algebraic.Cutwidth.Bisection.Internal.exists_bisectionBound {ξ : ℝ} (hξ : 0 < ξ) : ∃ (N₀ : ℕ), BisectionBound ξ N₀