Real rates and exact integer parameter choices

Rational density and the Archimedean property turn every real rate below one and positive additive coefficient error into a rational rate and an integer precision. Rounding the exponent upward covers the real copy budget.

theorem Algebraic.MassProduction.Nonuniform.existsRealCoefficientParameters {gamma epsilon : ℝ} (nonnegative : 0 ≤ gamma) (proper : gamma < 1) (errorPositive : 0 < epsilon) : ∃ (numerator : ℕ) (denominator : ℕ) (precision : ℕ), numerator < denominator ∧ 0 < precision ∧ gamma < ↑numerator / ↑denominator ∧ (↑precision + 1) * ↑denominator ≤ (1 / (1 - gamma) + epsilon) * ↑precision * ↑(denominator - numerator)

Real rates and additive errors admit rational/integer parameters with strict room in both the copy range and the requested coefficient.

theorem Algebraic.MassProduction.Nonuniform.realCopyBudget_le {gamma : ℝ} {numerator denominator inputs copies : ℕ} (denominatorPositive : 0 < denominator) (rateBound : gamma ≤ ↑numerator / ↑denominator) (copiesBound : ↑copies ≤ 2 ^ (gamma * ↑inputs)) : copies ≤ 2 ^ (numerator * inputs / denominator + 1)

The power of two at the upward-rounded rational exponent covers every integer copy count allowed by a smaller real exponent.