Capacity and error arithmetic for one round of extraction

Sparse rounding provides a hash field covering both lengths. The condenser rate controls its output and hence the total seed length. Power identities verify the sharp leftover-hash budget and the sum of the two half-errors. Unary computation uses only existing bounded rounding and arithmetic rules.

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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)

theorem Algebraic.Cutwidth.Extractor.Internal.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)