Polynomial versus exponential growth

The arithmetic behind the threshold of the recursive compression argument (planning/compression-track.md, K3 step 4): for every polynomial Q over ℕ there is a constant K such that n ≥ 2 ^ (K + 1 + x) forces Q (x + log n) ≤ n + 1 (exists_threshold). The proof is elementary: a polynomial is bounded by its coefficient sum times the top power (polynomial_eval_le_sum_coeff_mul_pow), and A · σ ^ D ≤ 2 ^ σ as soon as σ ≥ A (D + 1) ^ (D + 1) (mul_pow_le_two_pow).

theorem MIPRE.Cost.polynomial_eval_le_sum_coeff_mul_pow (Q : Polynomial ℕ) {y : ℕ} (hy : 1 ≤ y) : Polynomial.eval y Q ≤ (∑ i ∈ Finset.range (Q.natDegree + 1), Q.coeff i) * y ^ Q.natDegree

A polynomial over ℕ is bounded by its coefficient sum times the top power.

theorem MIPRE.Cost.mul_pow_le_two_pow (A D σ : ℕ) (h : A * (D + 1) ^ (D + 1) ≤ σ) : A * σ ^ D ≤ 2 ^ σ

A · σ ^ D ≤ 2 ^ σ for σ ≥ A (D + 1) ^ (D + 1): with μ = σ / (D + 1), A σ ^ D ≤ A (D + 1) ^ D (μ + 1) ^ D ≤ μ (μ + 1) ^ D ≤ (μ + 1) ^ (D + 1) ≤ 2 ^ (μ (D + 1)) ≤ 2 ^ σ.

theorem MIPRE.Cost.exists_threshold (Q : Polynomial ℕ) : ∃ (K : ℕ), ∀ (x n : ℕ), 2 ^ (K + 1 + x) ≤ n → Polynomial.eval (x + n.size) Q ≤ n + 1

The threshold lemma. For a polynomial Q, there is a constant K such that n ≥ 2 ^ (K + 1 + x) implies Q (x + log n) ≤ n + 1 (with log n = Nat.size n). This is what makes the threshold r e = 2 ^ (K + 1 + esize e) of the compression argument work: above it, every polynomial overhead in esize e + log n is at most n + 1.