Absorbing polynomial costs into n ^ λ

The two arithmetic facts the accounting of the compressor's output rests on. Its verifier at level n has to be n-bounded (Verifier.IsBounded n): running times at every index m ≥ 2 at most m ^ n · (|d| + 1) ^ n, and a description of size at most n. What the construction supplies is a running time polynomial in the index, the level and the input size, and a description of size polynomial in log n plus the half of n the criterion's slack leaves. Both are absorbed once n is past a threshold depending only on the polynomials:

• PolyBounded.absorb: for F polynomially bounded, F ((m + n + 1) · y) ≤ m ^ n · y ^ n for all m ≥ 2, y ≥ 1 and n past a threshold. The argument (m + n + 1) · y is what every cost is bounded by once each of its atoms — the index, the level, the input size — is replaced by the largest.
• PolyBounded.absorb_log: for g polynomially bounded, 2 · g (a + b · size n) ≤ n for n past a threshold: a polynomial in the length of n is eventually half of n.

Both are the parameter inequality of lem:lambda-bound in a coarser form; log_lt_div from its proof is the step with content.

theorem MIPRE.Cost.size_le_log_add_one (n : ℕ) : n.size ≤ Nat.log 2 n + 1

size n ≤ log₂ n + 1.

theorem MIPRE.Cost.PolyBounded.two_pow_size (K D : ℕ) : PolyBounded fun (n : ℕ) => 2 ^ (K + D * n.size)

2 ^ (K + D · size n) is polynomially bounded in n.

theorem MIPRE.Cost.PolyBounded.absorb {F : ℕ → ℕ} (hF : PolyBounded F) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ∀ (m : ℕ), 2 ≤ m → ∀ (y : ℕ), 1 ≤ y → F ((m + n + 1) * y) ≤ m ^ n * y ^ n

Absorption into m ^ n. A polynomially bounded function of (m + n + 1) · y is below m ^ n · y ^ n for every index m ≥ 2 and every y ≥ 1, once the level n is past a threshold depending on the polynomial alone.

theorem MIPRE.Cost.PolyBounded.absorb_log {g : ℕ → ℕ} (hg : PolyBounded g) (a b : ℕ) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → 2 * g (a + b * n.size) ≤ n

A polynomial in the length of n is eventually half of n.