The finite ordinary Gamma extractor

At target width b, use the selected near-halving construction on 8*b source bits and keep exactly its first b output coordinates. The complete Boolean seed retains all level seeds and the final one-shot pair once. Output coverage holds on every input size; the statistical guarantee uses the separate size guard. The encoded evaluator is a separate layer.

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

The complete number of Boolean seed bits used by the selected construction.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.gammaBlockExtractor (b : ℕ) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) (j : Fin b) : Bool

The actual near-halving Boolean extractor, truncated to the desired output length.

Equations

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