The Gamma program with a fixed polylogarithmic seed budget

The input and seed are ordinary Boolean vectors. Run the actual total string program and read its output coordinates, with the same total false default used by the bitstring APIs. The seed budget is an explicit cubic polynomial in the ceiling input logarithm; the extra seed suffix is ignored on valid sizes while remaining part of the retained seed in statistical tests.

def Algebraic.Cutwidth.Extractor.gammaBlockSeedBudget (b : ℕ) : ℕ

A simple uniform seed budget covering the actual selected seed length at valid sizes.

Equations

• Algebraic.Cutwidth.Extractor.gammaBlockSeedBudget b = 2 ^ 27 * Algebraic.Cutwidth.Extractor.gammaBlockLog b ^ 3

def Algebraic.Cutwidth.Extractor.gammaBlockPaddedExtractor (b : ℕ) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBudget b) → Bool) (j : Fin b) : Bool

Read the actual Gamma program on a Boolean source and a fixed-budget Boolean seed.

Equations

• Algebraic.Cutwidth.Extractor.gammaBlockPaddedExtractor b x seed j = (Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime b (List.ofFn x) (List.ofFn seed))[↑j]?.getD false