Finite bounds for the explicit sparse parameter choice

Ceiling division covers the source bits; rounding to a power of three costs at most another factor of three. The logarithmic slack then pays for the extension-degree and entropy factors in the normalized degree-loss bound.

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserBudget_pos (n k e : ℕ) : 0 < explicitCondenserBudget n k e

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserFieldBits_pos (n k e u : ℕ) : 0 < sparseFieldBits u (explicitCondenserBudget n k e)

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserPowerBits_pos (n k e : ℕ) {u : ℕ} (rate : 0 < u) : 0 < sparsePowerBits u (explicitCondenserBudget n k e)

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenserExtensionExponent_pos (n k e u : ℕ) : 0 < explicitCondenserExtensionExponent n k e u

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_degree_lower (n k e u : ℕ) : 3 ≤ explicitCondenserExtensionDegree n k e u

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_source_capacity (n k e u : ℕ) : n ≤ sparseFieldBits u (explicitCondenserBudget n k e) * explicitCondenserExtensionDegree n k e u

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_degree_le (n k e u : ℕ) : explicitCondenserExtensionDegree n k e u ≤ 9 * (n + 1)

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_entropy_capacity (n k e : ℕ) {u : ℕ} (rate : 0 < u) : k ≤ sparsePowerBits u (explicitCondenserBudget n k e) * condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e))

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_fieldBits_le (n k e u : ℕ) : sparseFieldBits u (explicitCondenserBudget n k e) ≤ 6 * (u + 1) * explicitCondenserBudget n k e

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_output_rate (n k e u : ℕ) : u * (condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e)) * sparseFieldBits u (explicitCondenserBudget n k e)) ≤ (u + 1) * k + u * sparseFieldBits u (explicitCondenserBudget n k e)

theorem Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_error_budget (n k e u : ℕ) : explicitCondenserExtensionDegree n k e u * k * 2 ^ e ≤ 2 ^ explicitCondenserBudget n k e