Positive rational exponent scales

This module exposes natural-number versions of the rational exponents used in hardness magnification. Floor and ceiling differ by at most one in the exponent, so their powers of two differ by at most a factor of two. It also provides the exact power-of-two input-length identity for a rounded N^(1+epsilon) bound.

theorem Complexity.PositiveRationalScale.value_pos (scale : PositiveRationalScale) : 0 < scale.value

Every represented rational scale is strictly positive.

theorem Complexity.PositiveRationalScale.eventually_atZeroFromPositive_iff {predicate : PositiveRationalScale → Prop} : (∀ᶠ (scale : PositiveRationalScale) in atZeroFromPositive, predicate scale) ↔ ∃ (cutoff : PositiveRationalScale), ∀ scale ≤ cutoff, predicate scale

A property holds for all sufficiently small positive rational scales exactly when it holds below one positive rational cutoff.

@[simp]

theorem Complexity.PositiveRationalScale.floorMul_zero (scale : PositiveRationalScale) : scale.floorMul 0 = 0

Scaling zero gives zero under floor rounding.

@[simp]

theorem Complexity.PositiveRationalScale.ceilMul_zero (scale : PositiveRationalScale) : scale.ceilMul 0 = 0

Scaling zero gives zero under ceiling rounding.

theorem Complexity.PositiveRationalScale.floorMul_mono (scale : PositiveRationalScale) : Monotone scale.floorMul

Floor-scaled multiplication is monotone in the natural argument.

theorem Complexity.PositiveRationalScale.floorMul_add_le (scale : PositiveRationalScale) (first second : ℕ) : scale.floorMul first + scale.floorMul second ≤ scale.floorMul (first + second)

The sum of two floor-rounded scaled exponents does not exceed the floor-rounded scale of their sum.

theorem Complexity.PositiveRationalScale.tendsto_floorMul_atTop (scale : PositiveRationalScale) : Filter.Tendsto scale.floorMul Filter.atTop Filter.atTop

The floor-scaled exponent tends to infinity for every positive rational scale.

theorem Complexity.PositiveRationalScale.eventually_coefficient_mul_succ_le_two_pow (coefficient : ℕ) : ∀ᶠ (exponent : ℕ) in Filter.atTop, coefficient * (exponent + 1) ≤ 2 ^ exponent

Every fixed multiple of n + 1 is eventually bounded by 2^n.

theorem Complexity.PositiveRationalScale.eventually_coefficient_mul_succ_pow_le_two_pow (coefficient degree : ℕ) : ∀ᶠ (exponent : ℕ) in Filter.atTop, coefficient * (exponent + 1) ^ degree ≤ 2 ^ exponent

Every fixed coefficient times a fixed power of n + 1 is eventually bounded by the binary exponential 2^n.

theorem Complexity.PositiveRationalScale.eventually_coefficient_mul_succ_pow_le_powFloor (scale : PositiveRationalScale) (coefficient degree : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, coefficient * (n + 1) ^ degree ≤ scale.powFloor n

Every fixed polynomial is eventually bounded by a floor-rounded binary exponential at any positive rational scale.

theorem Complexity.PositiveRationalScale.ceilMul_mono (scale : PositiveRationalScale) : Monotone scale.ceilMul

Ceiling-scaled multiplication is monotone in the natural argument.

theorem Complexity.PositiveRationalScale.denominator_mul_floorMul_le (scale : PositiveRationalScale) (n : ℕ) : scale.denominator * scale.floorMul n ≤ scale.numerator * n

Floor rounding never exceeds the exact scaled numerator after restoring the denominator.

theorem Complexity.PositiveRationalScale.numerator_mul_le_denominator_mul_ceilMul (scale : PositiveRationalScale) (n : ℕ) : scale.numerator * n ≤ scale.denominator * scale.ceilMul n

Ceiling rounding covers the exact scaled numerator after restoring the denominator.

theorem Complexity.PositiveRationalScale.floorMul_le_ceilMul (scale : PositiveRationalScale) (n : ℕ) : scale.floorMul n ≤ scale.ceilMul n

Floor rounding is no larger than ceiling rounding.

theorem Complexity.PositiveRationalScale.ceilMul_le_floorMul_add_one (scale : PositiveRationalScale) (n : ℕ) : scale.ceilMul n ≤ scale.floorMul n + 1

Floor and ceiling rounding differ by at most one.

theorem Complexity.PositiveRationalScale.floorMul_pos_of_denominator_le_numerator_mul (scale : PositiveRationalScale) {n : ℕ} (hlarge : scale.denominator ≤ scale.numerator * n) : 0 < scale.floorMul n

Once the unrounded numerator reaches the denominator, its floor-scaled value is positive.

theorem Complexity.PositiveRationalScale.powFloor_pos (scale : PositiveRationalScale) (n : ℕ) : 0 < scale.powFloor n

Rounded-down powers of two are positive.

theorem Complexity.PositiveRationalScale.powCeil_pos (scale : PositiveRationalScale) (n : ℕ) : 0 < scale.powCeil n

Rounded-up powers of two are positive.

theorem Complexity.PositiveRationalScale.powFloor_mono (scale : PositiveRationalScale) : Monotone scale.powFloor

Rounded-down powers are monotone in the natural argument.

theorem Complexity.PositiveRationalScale.powFloor_mul_le_powFloor_add (scale : PositiveRationalScale) (first second : ℕ) : scale.powFloor first * scale.powFloor second ≤ scale.powFloor (first + second)

The product of two floor-rounded binary powers is bounded by the rounded power at the sum of their arguments.

theorem Complexity.PositiveRationalScale.powFloor_pow_le_mul (scale : PositiveRationalScale) (n multiplier : ℕ) : scale.powFloor n ^ multiplier ≤ scale.powFloor (multiplier * n)

A fixed power of a floor-rounded binary power is bounded by scaling the natural argument by the same multiplier.

theorem Complexity.PositiveRationalScale.powCeil_mono (scale : PositiveRationalScale) : Monotone scale.powCeil

Rounded-up powers are monotone in the natural argument.

theorem Complexity.PositiveRationalScale.powFloor_le_powCeil (scale : PositiveRationalScale) (n : ℕ) : scale.powFloor n ≤ scale.powCeil n

Rounding the exponent down gives no larger a power than rounding it up.

theorem Complexity.PositiveRationalScale.powCeil_le_two_mul_powFloor (scale : PositiveRationalScale) (n : ℕ) : scale.powCeil n ≤ 2 * scale.powFloor n

Changing floor to ceiling costs at most a factor of two for binary exponentials.

@[simp]

theorem Complexity.PositiveRationalScale.onePlusCeilPow_eq_mul (scale : PositiveRationalScale) (n : ℕ) : scale.onePlusCeilPow n = 2 ^ n * scale.powCeil n

The rounded N^(1+scale) bound factors into its linear and fractional binary powers.

theorem Complexity.PositiveRationalScale.two_pow_le_onePlusCeilPow (scale : PositiveRationalScale) (n : ℕ) : 2 ^ n ≤ scale.onePlusCeilPow n

The rounded N^(1+scale) bound is at least the raw input length N.

@[simp]

theorem Complexity.PositiveRationalScale.onePlusCeilPowAtLength_pow (scale : PositiveRationalScale) (n : ℕ) : scale.onePlusCeilPowAtLength (2 ^ n) = scale.onePlusCeilPow n

On an exact 2^n-bit input, recovering arity from length gives the intended rounded N^(1+scale) bound exactly.