Rounding and degree-budget arithmetic for sparse field sizes

The upper logarithm rounds the field bit length to twice a power of three. Ceiling division controls the coordinate count. The rate inequality is integer-valued, so no logarithm or real rounding convention is hidden.

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

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

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

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

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

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

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

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

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

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

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