A binary condenser with parameters selected from the requested bounds

The source-length bound n, entropy budget k, inverse-error exponent e, and rate parameter u determine all dimensions and iteration counts of the existing runtime program. Its output consists of coordinate bits, without the seed. The paired evaluator reads the four parameters from word lengths.

The decoded map interprets these same output bits in the selected binary field. No source-length or parameter promises enter these total definitions; the statistical guarantees impose their hypotheses separately.

def Algebraic.Cutwidth.Extractor.explicitCondenserBits (n k e u : ℕ) (source seed : List Bool) : List Bool

Run the uniform binary program at the explicitly selected parameters.

Equations

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

def Algebraic.Cutwidth.Extractor.explicitCondenserEval (z : List Bool) : List Bool

Codec: pair (pair source seed) (pair (pair n k) (pair e u)), with parameters given by the lengths of their words.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.decodedExplicitCondenser (n k e u : ℕ) (bits : List Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) : Fin (condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e))) → AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))

The actual scheduled output, interpreted as coordinates in the selected field.

Equations

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