A fully specified finite recursive strong extractor

The initial condenser, all internal condensers, their actual rounded widths, and the final one-shot extractor are specified by the numerical definitions. The explicit reserve 4096*(L+E+1) discharges every level's entropy budget. The resulting map outputs 2^h blocks of L field bits, with all seeds retained in the statistical test.

The construction uses the recursive condensation and splitting method of Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. Our constant-rate schedule pays a factor of four in entropy per level; it does not assert their sharper entropy bound. The seed-length estimate and a uniform encoded evaluator are separate layers. Finite-field instances are supplied by the proved cardinality of each binary quotient.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractor_weighted [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] (n h Q E ell : ℕ) (budget : 3 * (24 * explicitCondenserBudget (scheduledBlockInitialWidth n h Q E) (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) (reserve : ell + 2 * E ≤ Q) : WeightedStrongSeededExtractor (scheduledBlockExtractor n h Q E ell) (2 ^ recursiveBlockEntropy h Q 0) ((3 * 2 ^ h - 1) * (2 ^ E)⁻¹)

The specified component maps give strong extraction whenever one global reserve budget and the final one-shot entropy requirement are satisfied.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractor_dyadic [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (depth : h ≤ L) : WeightedStrongSeededExtractor (scheduledBlockExtractor n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L) (2 ^ recursiveBlockEntropy h (recursiveBlockReserve L (e + h + 2)) 0) (2 ^ e)⁻¹

The explicit reserve and local exponent e+h+2 give total error 2^(-e). The only numerical premises bound the source logarithm and recursion depth.