A finite parameter choice with source capacity, rate, and error bounds

For T = e + clog 2 (9*(n+1)*(k+1)) + 1, retain the sparse choices b = sparseFieldBits u T and r = sparsePowerBits u T. Round the extension degree d to a power of three above both three and ceil(n/b). Then b*d covers the source, d is linear in n, and the integer error budget pays for loss 2^(-e). The coordinate count is condenserCoordinates k r.

These explicit rounding choices are our deduction from the finite sparse rate and loss bounds in Parameters.Sparse, whose source credit is given there. This layer contains exact natural-number inequalities. Its sibling Explicit.Unary supplies uniform certificates for constructing the numerical parameters; no asymptotic or extractor statement is asserted here.

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

The error and degree budget is positive even when all inputs are zero.

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

Every selected base field has a positive bit width.

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

A positive rate parameter leaves positive capacity in every coordinate.

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

The selected extension exponent is always positive.

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

The extension degree is at least three, as required for the expansion regime.

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

The coefficient rectangle holds the entire n-bit source.

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

Rounding the extension degree costs at most a linear factor in source length.

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

The selected number of coordinates carries at least k entropy bits.

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

The seed bit length is bounded by six times the rate-adjusted slack budget.

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

The coordinate output approaches rate 1+1/u, with one field element of slack.

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

The exact integer budget needed for inverse-power-of-two error.