Strong extraction with the actual constant-rate schedule

Instantiate the finite recursion with the initial rate-one condenser, the actual rate-three level maps, and the final one-shot extractor. The explicit reserve theorem discharges every entropy budget using only the chosen depth and an upper bound on the original source length's binary logarithm.

theorem Algebraic.Cutwidth.Extractor.Internal.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)⁻¹)

theorem Algebraic.Cutwidth.Extractor.Internal.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)⁻¹