Uniform computation of the fixed asymptotic extractor family

The family depth is a polynomial-time unary function of the input length. For sufficiently large lengths, its depth fits the finite schedule, so the total bit program computes exactly the specified asymptotic extractor on every source and canonical seed word. This ties the asymptotic statistical map to a single polynomial-time machine for each fixed family.

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

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