From bounded helpful sets to a prescribed cut reduction

This is the accumulation step in Monien and Preis's cubic bisection proof. It assumes the local helpful-set lemma and proves the iteration, size bound, and preservation of the density condition. It does not establish the local helpful-set lemma itself.

theorem Algebraic.Cutwidth.Bisection.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) : ∃ X ⊆ S, X.card ≤ k * M ∧ ↑k ≤ helpfulness H S X

If every remaining side of density above a has a helpful set of size at most M, a margin of k yields a union of at most k M vertices whose helpfulness is at least k. The last move may exceed the target reduction.