A finite entropy budget for splitting the paired condenser

Let H be the actual condenser half-width and b its field seed width. The coordinate count proves k ≤ 2*H. Together with the output-rate bound, the sufficient budget u*(b+2*(s+E)) ≤ (u-1)*k gives both s ≤ H and H+s+E ≤ k. The condenser error exponent e and splitting error exponent E remain independent.

These are arithmetic deductions for our sparse parameter choice. The two target inequalities are the entropy requirements of the splitting step in Chattopadhyay--Goodman--Liao, Corollary 5.4 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. This layer establishes one finite level's budget; Recursion.Scheduled chooses the recursive sequence and bounds its total seed length (eventually_polylogBlockSeedBits_le).

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

The actual two-half output has capacity for all k input entropy bits.

theorem Algebraic.Cutwidth.Extractor.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

A field-width budget supplies both entropy inequalities needed for splitting.

theorem Algebraic.Cutwidth.Extractor.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

The explicit upper bound on field width gives a sufficient budget without sparse rounding.

theorem Algebraic.Cutwidth.Extractor.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

The maximal next entropy k-H-E fits in one half and exactly exhausts the split budget. The sufficient field-width budget ensures that natural subtraction does not truncate.