Sparse field sizes preserving the condenser output rate

For a target rate 1 + 1/u, round (u+1)*T up to a field bit length b = 2 * 3^s, and then choose the powering bit length r = b-T. The rate inequality u*b ≤ (u+1)*r survives this sparse rounding. For m = ceil(k/r), the coordinate count is at most k, and the output length satisfies u*(m*b) ≤ (u+1)*k + u*b.

These finite inequalities are a parameter choice for the binomial modulus family. They adapt the field-size and powering tradeoff in Cheraghchi's 2010 thesis, Corollary 2.23, to a sparse grid; this grid choice is our deduction, not a statement attributed to that source: https://arxiv.org/pdf/1107.4709. The normalized degree loss is at most error whenever D*k ≤ error*2^T. No asymptotic bound, field construction, or runtime certificate is claimed here.

theorem Algebraic.Cutwidth.Extractor.sparseFieldBits_lower (u T : ℕ) : (u + 1) * T ≤ sparseFieldBits u T

The selected field bit length covers the entire rate and error budget.

theorem Algebraic.Cutwidth.Extractor.sparseFieldBits_upper {u T : ℕ} (positive : 0 < T) : sparseFieldBits u T ≤ 6 * ((u + 1) * T)

Sparse rounding costs at most a fixed factor in field bit length.

theorem Algebraic.Cutwidth.Extractor.sparsePowerBits_add {u T : ℕ} : sparsePowerBits u T + T = sparseFieldBits u T

The powering and slack bit lengths add up to the field bit length.

theorem Algebraic.Cutwidth.Extractor.sparsePowerBits_pos {u T : ℕ} (rate : 0 < u) (positive : 0 < T) : 0 < sparsePowerBits u T

Positive rate and slack parameters leave a positive powering bit length.

theorem Algebraic.Cutwidth.Extractor.sparsePowerBits_rate (u T : ℕ) : u * sparseFieldBits u T ≤ (u + 1) * sparsePowerBits u T

The exact integer inequality expressing the target output rate 1+1/u.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinates_capacity {k r : ℕ} (positive : 0 < r) : k ≤ r * condenserCoordinates k r

Ceiling division supplies enough coordinates to carry all k bits.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinates_le {k r : ℕ} (positive : 0 < r) : condenserCoordinates k r ≤ k

A positive bit capacity per coordinate requires at most k coordinates.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinates_output {u k r b : ℕ} (rate : u * b ≤ (u + 1) * r) : u * (condenserCoordinates k r * b) ≤ (u + 1) * k + u * b

Ceiling division costs at most one additional field element in output length.

theorem Algebraic.Cutwidth.Extractor.condenserCoordinates_loss {D k r T : ℕ} {error : ℝ} (positive : 0 < r) (budget : ↑D * ↑k ≤ error * 2 ^ T) : ↑((D - 1) * (2 ^ r - 1) * condenserCoordinates k r) / 2 ^ (r + T) ≤ error

The elementary degree-loss budget after choosing a power-of-two field size.

theorem Algebraic.Cutwidth.Extractor.sparseCondenser_output {u T k : ℕ} : u * (condenserCoordinates k (sparsePowerBits u T) * sparseFieldBits u T) ≤ (u + 1) * k + u * sparseFieldBits u T

The output-rate bound specialized to the sparse field bit length.

theorem Algebraic.Cutwidth.Extractor.sparseCondenser_loss {u T D k : ℕ} {error : ℝ} (rate : 0 < u) (positive : 0 < T) (budget : ↑D * ↑k ≤ error * 2 ^ T) : ↑((D - 1) * (2 ^ sparsePowerBits u T - 1) * condenserCoordinates k (sparsePowerBits u T)) / 2 ^ sparseFieldBits u T ≤ error

The exact normalized loss bound specialized to the sparse field bit length.