Rebalancing through a prescribed endpoint decomposition

The endpoint decomposition of Fomin and Høie and the median-edge ordering give a logarithmic-cost substitute for Monien and Preis's rebalancing lemma. The cost depends on the side's order, which still suffices when accumulated helpful moves have a logarithmic total gain.

theorem Algebraic.Cutwidth.Bisection.Internal.exists_subset_cut_le {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (regular : H.IsRegularOfDegree 3) {k : ℕ} (hk : k ≤ S.card) : ∃ T ⊆ S, T.card = k ∧ (H.cutFinset T).card ≤ max (H.cutFinset S).card (S.card / 3 + 1) + Nat.clog 2 S.card + 2

theorem Algebraic.Cutwidth.Bisection.Internal.exists_rebalancing_set {W : Type} [Fintype W] (H : SimpleGraph W) (S : Finset W) (regular : H.IsRegularOfDegree 3) (dense : S.card < 3 * (H.cutFinset S).card) {k : ℕ} (hk : k ≤ S.card) : ∃ X ⊆ S, X.card = k ∧ -(↑(Nat.clog 2 S.card) + 2) ≤ helpfulness H S X