Elementary eventual growth bounds for mass production

The manuscript repeatedly uses that a fixed positive linear gap between binary exponents absorbs every fixed polynomial factor. This file packages that step in exact natural-number form, with eventual quantifiers only at the outer boundary.

theorem Algebraic.MassProduction.Growth.div_add_div_le (left right divisor : ℕ) (divisorPositive : 0 < divisor) : left / divisor + right / divisor ≤ (left + right) / divisor

The sum of two floored quotients is at most the floor of the sum.

theorem Algebraic.MassProduction.Growth.eventually_const_mul_pow_le_two_pow (constant degree : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, constant * n ^ degree ≤ 2 ^ n

Every fixed natural polynomial monomial, including a fixed coefficient, is eventually bounded by the matching binary exponential.

theorem Algebraic.MassProduction.Growth.eventually_const_mul_pow_le_two_pow_div (constant degree divisor : ℕ) (divisorPositive : 0 < divisor) : ∀ᶠ (n : ℕ) in Filter.atTop, constant * n ^ degree ≤ 2 ^ (n / divisor)

A fixed polynomial is also absorbed by the exponential carried by any fixed positive fraction n / divisor of the input length.

theorem Algebraic.MassProduction.Growth.eventually_mul_two_pow_rational_le (constant degree low high denominator : ℕ) (denominatorPositive : 0 < denominator) (gap : low < high) : ∀ᶠ (n : ℕ) in Filter.atTop, constant * n ^ degree * 2 ^ (low * n / denominator) ≤ 2 ^ (high * n / denominator)

A strict gap between two rational binary exponents absorbs a fixed polynomial coefficient. Natural division implements both floors.

theorem Algebraic.MassProduction.Growth.eventually_mul_two_pow_rational_le_shannonScale (constant degree numerator denominator : ℕ) (denominatorPositive : 0 < denominator) (proper : numerator < denominator) : ∀ᶠ (n : ℕ) in Filter.atTop, constant * n ^ degree * 2 ^ (numerator * n / denominator) ≤ 2 ^ n / n

If a rational exponent is strictly below one, the same exponential margin absorbs both a fixed polynomial and the denominator n in the sharp Shannon scale 2^n / n.

theorem Algebraic.MassProduction.Growth.div_le_four_mul_double_div (value divisor : ℕ) (divisorPositive : 0 < divisor) (twoDivisorFits : 2 * divisor ≤ value) : value / divisor ≤ 4 * (value / (2 * divisor))

Doubling a positive denominator changes a sufficiently nonzero natural quotient by at most a factor four. This coarse floor-stable form is useful when comparing equal-block resource terms with 2^n / n.

theorem Algebraic.MassProduction.Growth.mul_div_le_two_mul_mul_div (constant value divisor : ℕ) (divisorPositive : 0 < divisor) (divisorFits : divisor ≤ value) : constant * value / divisor ≤ 2 * constant * (value / divisor)

Pulling a fixed coefficient outside natural division costs at most a factor two once the quotient is nonzero.