A recursive strong extractor with logarithmic seed and sublinear entropy

Fix natural family parameters a,e. At input length n, take L=clog 2 (n+1), depth h=a*clog 2 (L+1), and local error exponent e+h+2. The specified recursive map eventually strongly extracts at error 2^(-e), using at most 16384*L seed bits. Its initial entropy in bits is little-o of n; its output lies between L^(a+1) and 2^a*(L+1)^(a+1). The source support threshold is two raised to the entropy-bit threshold.

The finite construction follows 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/. This constant-rate schedule has its own coarser entropy bound. The limit estimates use Cslib's natural exponential-versus-polynomial theorem and Mathlib's logarithm and little-o APIs. Scheduled.Program gives a uniform encoded evaluator for the complete variable-depth family (scheduledBlockExtractorEval_mem_FP).

theorem Algebraic.Cutwidth.Extractor.eventually_polylogBlockDepth_le (a : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, polylogBlockDepth a n ≤ polylogBlockLength n

For each fixed depth multiplier, the raw depth eventually fits the logarithmic budget.

theorem Algebraic.Cutwidth.Extractor.polylogBlockEntropy_isLittleO (a e : ℕ) : (fun (n : ℕ) => ↑(polylogBlockEntropy a e n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

The actual initial entropy in bits is sublinear for each fixed family.

theorem Algebraic.Cutwidth.Extractor.eventually_polylogBlockEntropy_le (a e : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, polylogBlockEntropy a e n ≤ n

Eventually the required entropy fits within the source's n Boolean coordinates.

theorem Algebraic.Cutwidth.Extractor.eventually_polylogBlockSeedBits_le (a e : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, polylogBlockSeedBits a e n ≤ 16384 * polylogBlockLength n

The actual retained seeds eventually occupy at most a fixed multiple of the input logarithm.

theorem Algebraic.Cutwidth.Extractor.card_polylogBlockSeeds (a e n : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] : Fintype.card (PolylogBlockSeeds a e n) = 2 ^ polylogBlockSeedBits a e n

The named seed alphabet has exactly the stated binary cardinality, at every input length.

theorem Algebraic.Cutwidth.Extractor.polylogBlockOutputBits_bounds (a n : ℕ) : polylogBlockLength n ^ (a + 1) ≤ polylogBlockOutputBits a n ∧ polylogBlockOutputBits a n ≤ 2 ^ a * (polylogBlockLength n + 1) ^ (a + 1)

Finite lower and upper bounds on the number of bits output across all leaves.

theorem Algebraic.Cutwidth.Extractor.eventually_polylogBlockExtractor (a e : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] : ∀ᶠ (n : ℕ) in Filter.atTop, WeightedStrongSeededExtractor (polylogBlockExtractor a e n) (2 ^ polylogBlockEntropy a e n) (2 ^ e)⁻¹

Every fixed family eventually satisfies strong extraction with the actual retained seeds.