Strong extraction with near-halving entropy budgets

The actual recursively paired condensers, followed by shared one-shot leaf extraction, form a strong extractor whenever the initial capacity and one finite reserve inequality hold. The recurrence preserves at least seven eighths of the initial entropy in the total output. Every seed is retained in the joint statistical guarantee, including the final pair shared by all leaves. An identity initialization spends no seed bits.

The condense/split method is from Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy: https://eccc.weizmann.ac.il/report/2021/075/. This depth-dependent rate and its conservative integer reserve are deductions for the present library. The short-seed parameter choice and uniform evaluator are separate layers.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockExtractor_weighted (n h Q E : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] (capacity : nearHalvingBlockEntropy h Q 0 ≤ n) (budget : 12 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget n (nearHalvingBlockEntropy h Q 0) E + 4 * E ≤ Q) : WeightedStrongSeededExtractor (nearHalvingBlockExtractor n h Q E) (2 ^ nearHalvingBlockEntropy h Q 0) ((3 * 2 ^ h - 1) * (2 ^ E)⁻¹)

The specified map strongly extracts with its explicit full recursive error bound.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockExtractor_dyadic (n h Q e : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] (capacity : nearHalvingBlockEntropy h Q 0 ≤ n) (budget : 12 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget n (nearHalvingBlockEntropy h Q 0) (e + h + 2) + 4 * (e + h + 2) ≤ Q) : WeightedStrongSeededExtractor (nearHalvingBlockExtractor n h Q (e + h + 2)) (2 ^ nearHalvingBlockEntropy h Q 0) (2 ^ e)⁻¹

A common local exponent e+h+2 pays for the complete recursion at error 2^(-e).