Finite parameters for one round of condensation and hashing

The condenser uses entropy ell+2*e, error exponent e+1, and rate parameter one. The second sparse field covers both the condensed output and the requested ell-bit prefix. The leftover-hash budget is exact, and the two half-errors add to 2^(-e). These calculations instantiate the condense-then-hash mechanism of Chattopadhyay--Goodman--Liao, Lemma 4.9 (https://eccc.weizmann.ac.il/report/2021/075/download/), using this library's explicit sparse condenser schedule and the sharp leftover bound.

The total seed bound is finite and explicit. No logarithmic asymptotic seed bound or recursive extractor construction is asserted. All three parameters and both actual half-degrees are uniformly polynomial-time in unary inputs. Only the existing bounded power-rounding rule is used; the exponentials that express support cardinality and error are not generated.

theorem Algebraic.Cutwidth.Extractor.oneShotCondenserOutputBits_le (n ell e : ℕ) : oneShotCondenserOutputBits n ell e ≤ 2 * (ell + 2 * e) + 2 * 3 ^ oneShotCondenserExponent n ell e

Rate parameter one bounds the condensed output by twice the entropy budget plus one condenser field element.

theorem Algebraic.Cutwidth.Extractor.oneShotHashBits_source_capacity (n ell e : ℕ) : oneShotCondenserOutputBits n ell e ≤ 2 * 3 ^ oneShotHashExponent n ell e

The hashing field has enough coefficient bits for the entire condensed word.

theorem Algebraic.Cutwidth.Extractor.oneShotHashBits_output_capacity (n ell e : ℕ) : ell ≤ 2 * 3 ^ oneShotHashExponent n ell e

The requested hash prefix fits in the hashing field.

theorem Algebraic.Cutwidth.Extractor.oneShotHashBits_le (n ell e : ℕ) : 2 * 3 ^ oneShotHashExponent n ell e ≤ 6 * (oneShotCondenserOutputBits n ell e + ell + 1)

Rounding the hashing field has a uniform constant-factor bound, including zero source and output lengths.

theorem Algebraic.Cutwidth.Extractor.oneShotSeedBits_le (n ell e : ℕ) : 2 * 3 ^ oneShotCondenserExponent n ell e + 2 * 3 ^ oneShotHashExponent n ell e ≤ 7 * (2 * 3 ^ oneShotCondenserExponent n ell e) + 12 * (ell + 2 * e) + 6 * ell + 6

A finite bound on the sum of the independent condenser and hash seed widths.

theorem Algebraic.Cutwidth.Extractor.oneShot_leftover_budget_eq (ell e : ℕ) : 2 ^ ell = 4 * (2 ^ (e + 1))⁻¹ ^ 2 * ↑(2 ^ (ell + 2 * e))

Entropy ell+2*e exactly pays the sharp leftover-hash budget at half of the requested final error.

theorem Algebraic.Cutwidth.Extractor.oneShot_leftover_budget (ell e : ℕ) : 2 ^ ell ≤ 4 * (2 ^ (e + 1))⁻¹ ^ 2 * ↑(2 ^ (ell + 2 * e))

Inequality form of the exact budget for the finite leftover-hash theorem.

theorem Algebraic.Cutwidth.Extractor.oneShot_half_errors (e : ℕ) : (2 ^ (e + 1))⁻¹ + (2 ^ (e + 1))⁻¹ = (2 ^ e)⁻¹

The condenser and hash each receive half of the total permitted error.

theorem Algebraic.Cutwidth.Extractor.oneShotCondenserExponent_unaryFn {n ell e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => oneShotCondenserExponent (n z) (ell z) (e z)

Uniform unary computation of the condenser's field exponent.

theorem Algebraic.Cutwidth.Extractor.oneShotCondenserOutputBits_unaryFn {n ell e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => oneShotCondenserOutputBits (n z) (ell z) (e z)

Uniform unary computation of the exact condensed output width.

theorem Algebraic.Cutwidth.Extractor.oneShotHashExponent_unaryFn {n ell e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => oneShotHashExponent (n z) (ell z) (e z)

Uniform unary computation of the hashing field exponent.

theorem Algebraic.Cutwidth.Extractor.oneShotCondenserHalfDegree_unaryFn {n ell e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => 3 ^ oneShotCondenserExponent (n z) (ell z) (e z)

The condenser's actual half-degree is polynomial-time by bounded rounding.

theorem Algebraic.Cutwidth.Extractor.oneShotHashHalfDegree_unaryFn {n ell e : List Bool → ℕ} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) : Complexity.UnaryFn fun (z : List Bool) => 3 ^ oneShotHashExponent (n z) (ell z) (e z)

The hashing field's actual half-degree is polynomial-time by bounded rounding.