One string program for each polylogarithmic-output extractor family

Fix the output exponent parameter and error exponent. The program reads a paired source and seed word, computes its requested logarithmic depth, and uses the total scheduled evaluator. Clipping affects only lengths where the raw requested depth exceeds the finite logarithmic budget; the checked asymptotic depth estimate shows that it is eventually inactive.

def Algebraic.Cutwidth.Extractor.polylogBlockExtractorProgram (a e : ℕ) (z : List Bool) : List Bool

Uniform bit program for the fixed family, on pair source seedWord.

Equations

• One or more equations did not get rendered due to their size.