Integer budgets for splitting the scheduled condenser

The coordinate capacity supplies a lower bound on the total output width. Its upper rate bound and a sufficient entropy budget then give both inequalities required to split the output into two conditional blocks.

theorem Algebraic.Cutwidth.Extractor.Internal.pair_split_of_budget {u H k b s E : ℕ} (positive : 0 < u) (capacity : k ≤ H + H) (rate : u * (H + H) ≤ (u + 1) * k + u * b) (budget : u * (b + 2 * (s + E)) ≤ (u - 1) * k) : s ≤ H ∧ H + s + E ≤ k

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserHalfWidth_capacity (n k e : ℕ) {u : ℕ} (rate : 0 < u) : k ≤ explicitCondenserHalfWidth n k e u + explicitCondenserHalfWidth n k e u

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserPair_split_budget (n k e u s E : ℕ) (rate : 1 < u) (budget : u * (sparseFieldBits u (explicitCondenserBudget n k e) + 2 * (s + E)) ≤ (u - 1) * k) : s ≤ explicitCondenserHalfWidth n k e u ∧ explicitCondenserHalfWidth n k e u + s + E ≤ k

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserPair_split_budget_of_bound (n k e u s E : ℕ) (rate : 1 < u) (budget : u * (6 * (u + 1) * explicitCondenserBudget n k e + 2 * (s + E)) ≤ (u - 1) * k) : s ≤ explicitCondenserHalfWidth n k e u ∧ explicitCondenserHalfWidth n k e u + s + E ≤ k

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserPair_next_entropy (n k e u E : ℕ) (rate : 1 < u) (budget : u * (sparseFieldBits u (explicitCondenserBudget n k e) + 2 * E) ≤ (u - 1) * k) : k - explicitCondenserHalfWidth n k e u - E ≤ explicitCondenserHalfWidth n k e u ∧ explicitCondenserHalfWidth n k e u + (k - explicitCondenserHalfWidth n k e u - E) + E = k