A uniform polynomial-time evaluator for each asymptotic extractor family

For fixed natural parameters a,e, one string function computes the entire recursive extractor from its source and seed word. For every sufficiently large source length, it agrees with the specified asymptotic extractor on all Boolean inputs and all canonical seeds. The seed codec is bijective at the exact proved seed length, so canonical words cover that entire seed space.

theorem Algebraic.Cutwidth.Extractor.polylogBlockExtractorProgram_mem_FP (a e : ℕ) : polylogBlockExtractorProgram a e ∈ Complexity.FP

The complete fixed-family bit program is polynomial-time in its source and seed word.

theorem Algebraic.Cutwidth.Extractor.eventually_polylogBlockExtractorProgram (a e : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (x : Fin n → Bool) (seeds : PolylogBlockSeeds a e n), polylogBlockExtractorProgram a e (Complexity.pair (List.ofFn x) (encodeScheduledBlockSeeds n (polylogBlockDepth a n) (polylogBlockReserve a e n) (polylogBlockErrorExponent a e n) (polylogBlockLength n) seeds)) = (List.ofFn fun (i : Fin (recursiveBlockCount 1 (polylogBlockDepth a n))) => List.ofFn fun (j : Fin (polylogBlockLength n)) => decide (polylogBlockExtractor a e n x seeds i j = 1)).flatten

At all sufficiently large lengths, the single program computes every coordinate of the specified family on all source inputs and canonically encoded seeds.