Parameters for one round of condensation and linear hashing

For output length ell and inverse-error exponent e, the entropy threshold is ell + 2*e. The condenser uses rate parameter one and error exponent e+1. Its output is embedded in a second sparse binary field large enough for both that output and the requested hash prefix. The two half-errors are intended to add to 2^(-e); the numerical theorems are separate.

def Algebraic.Cutwidth.Extractor.oneShotCondenserExponent (n ell e : ℕ) : ℕ

The sparse field exponent for the first, condensing stage.

Equations

• Algebraic.Cutwidth.Extractor.oneShotCondenserExponent n ell e = Algebraic.Cutwidth.Extractor.sparseFieldExponent 1 (Algebraic.Cutwidth.Extractor.explicitCondenserBudget n (ell + 2 * e) (e + 1))

def Algebraic.Cutwidth.Extractor.oneShotCondenserOutputBits (n ell e : ℕ) : ℕ

The exact bit length of the first stage's output.

Equations

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

def Algebraic.Cutwidth.Extractor.oneShotHashExponent (n ell e : ℕ) : ℕ

The hashing field covers the condensed word and requested output prefix.

Equations

• Algebraic.Cutwidth.Extractor.oneShotHashExponent n ell e = Algebraic.Cutwidth.Extractor.sparseFieldExponent 0 (max (Algebraic.Cutwidth.Extractor.oneShotCondenserOutputBits n ell e) ell)