Accumulating helpful moves #
The first step of Monien and Preis's bisection argument applies a bounded helpful-set lemma until the total cut reduction reaches a chosen target. The density margin preserves the local lemma's hypothesis at every step.
theorem
Algebraic.Cutwidth.Bisection.Internal.exists_helpful_set_of_margin
{W : Type}
[Fintype W]
(H : SimpleGraph W)
(S : Finset W)
{a : ℝ}
(ha : 0 ≤ a)
(M k : ℕ)
(margin : a * ↑S.card + ↑k < ↑(H.cutFinset S).card)
(find : ∀ T ⊆ S, a * ↑T.card < ↑(H.cutFinset T).card → ∃ X ⊆ T, X.card ≤ M ∧ 1 ≤ helpfulness H T X)
: