The parameter arithmetic of the compression theorem

Blueprint lem:compress-margin and lem:compress-tau (paper recursive.tex, the proof of thm:compression; ledger nodes 1.5.3, 1.5.5): the four stages of Compress are chained through a budget of margins, and these are the arithmetic facts about the imported constants that make each application of a soundness clause, taken contrapositively, land strictly inside the gap it is handed.

Write x = λn, (a₁, b₁) for the constants of introspection and (a₂, b₂) for those of answer reduction (a₁, a₂ ≥ 1, 0 < b₁, b₂ ≤ 1).

• ε₁(x) = (8 a₁ x^{a₁})^{-1/b₁} makes the introspection loss δ₁(ε₁, n) < 1/2 once x ≥ (4a₁)^{1/b₁} (intro_margin): the first term of δ₁ is exactly 1/8, the second at most 1/4.
• ε₂ = (ε₁ / (3 σ^{a₂} x^{μ a₂}))^{1/b₂} makes the first term of the answer-reduction loss δ₂(ε₂, n) exactly ε₁/3; the second, σ^{a₂} x^{-μ b₂}, is below ε₁/2 for μ large (exists_mu, the margin claim): with σ ≤ x^K, any μ b₂ ≥ K a₂ + a₁/b₁ + 1 works past a threshold on x. The paper fixes μ = ⌈max{C_intro, (9a₁ + 2a₂ C_intro)/(b₁ b₂)}⌉ and n ≥ 2; the threshold here is absorbed by C₀.
• 1/ε₂ is bounded by a fixed power of x (exists_eps2_lower), so a universal repetition exponent τ brings the repetition bound exp(-c ε₂^{13} k / (B + 1)) below 1/2 for any k ≥ z^τ and B ≤ z^β, z = λn + 1, for n ≥ τ (exists_tau).

Everything is real arithmetic with Real.rpow; nothing depends on the verifiers.

The introspection margin

noncomputable def MIPRE.Pipeline.eps1 (a b x : ℝ) : ℝ

ε₁(x) = (8 a x^a)^{-1/b}.

Equations

• MIPRE.Pipeline.eps1 a b x = (8 * a * x ^ a) ^ (-(1 / b))

theorem MIPRE.Pipeline.eps1_pos {a b x : ℝ} (ha : 1 ≤ a) (hx : 0 < x) : 0 < eps1 a b x

theorem MIPRE.Pipeline.eps1_le_one {a b x : ℝ} (ha : 1 ≤ a) (hb : 0 < b) (hx : 1 ≤ x) : eps1 a b x ≤ 1

theorem MIPRE.Pipeline.eps1_rpow {a b x : ℝ} (ha : 1 ≤ a) (hb : 0 < b) (hx : 0 < x) : eps1 a b x ^ b = (8 * a * x ^ a)⁻¹

ε₁^b = (8 a x^a)⁻¹.

theorem MIPRE.Pipeline.eps1_eq {a b x : ℝ} (ha : 1 ≤ a) (hx : 0 < x) : eps1 a b x = (8 * a) ^ (-(1 / b)) * x ^ (-(a / b))

ε₁(x) = (8a)^{-1/b} · x^{-a/b}.

theorem MIPRE.Pipeline.intro_margin {a b x : ℝ} (ha : 1 ≤ a) (hb : 0 < b) (hx : 1 ≤ x) (hx' : (4 * a) ^ (1 / b) ≤ x) : a * (x ^ a * eps1 a b x ^ b + x ^ (-b)) < 1 / 2

The introspection step lands below 1/2: δ₁(ε₁, n) < 1/2 once x = λn is at least (4a)^{1/b}.

The margin claim

theorem MIPRE.Pipeline.exists_mu {a₁ b₁ a₂ b₂ : ℝ} (ha₁ : 1 ≤ a₁) (ha₂ : 1 ≤ a₂) (hb₂ : 0 < b₂) (K C : ℕ) : ∃ (mu : ℕ), C ≤ mu ∧ ∃ (N : ℕ), ∀ (x : ℝ), ↑N ≤ x → ∀ (s : ℝ), 1 ≤ s → s ≤ x ^ ↑K → s ^ a₂ * x ^ (-(↑mu * b₂)) < eps1 a₁ b₁ x / 2

The margin claim (blueprint lem:compress-margin). Given the constants of introspection and answer reduction, a bound σ ≤ x^K on the size parameter and a lower bound C wanted of μ, there is a universal μ ≥ C and a threshold N such that for x ≥ N, σ^{a₂} x^{-μ b₂} < ε₁(x) / 2.

The answer-reduction step

noncomputable def MIPRE.Pipeline.eps2 (a₁ b₁ a₂ b₂ : ℝ) (mu : ℕ) (s x : ℝ) : ℝ

ε₂ = (ε₁ / (3 σ^{a₂} x^{μ a₂}))^{1/b₂}.

Equations

• MIPRE.Pipeline.eps2 a₁ b₁ a₂ b₂ mu s x = (MIPRE.Pipeline.eps1 a₁ b₁ x / (3 * s ^ a₂ * x ^ (↑mu * a₂))) ^ (1 / b₂)

theorem MIPRE.Pipeline.eps2_pos {a₁ b₁ a₂ b₂ : ℝ} {mu : ℕ} {s x : ℝ} (ha₁ : 1 ≤ a₁) (hs : 0 < s) (hx : 0 < x) : 0 < eps2 a₁ b₁ a₂ b₂ mu s x

theorem MIPRE.Pipeline.eps2_le_one {a₁ b₁ a₂ b₂ : ℝ} {mu : ℕ} {s x : ℝ} (ha₁ : 1 ≤ a₁) (hb₁ : 0 < b₁) (ha₂ : 1 ≤ a₂) (hb₂ : 0 < b₂) (hs : 1 ≤ s) (hx : 1 ≤ x) : eps2 a₁ b₁ a₂ b₂ mu s x ≤ 1

theorem MIPRE.Pipeline.eps2_rpow {a₁ b₁ a₂ b₂ : ℝ} {mu : ℕ} {s x : ℝ} (ha₁ : 1 ≤ a₁) (hb₂ : 0 < b₂) (hs : 0 < s) (hx : 0 < x) : eps2 a₁ b₁ a₂ b₂ mu s x ^ b₂ = eps1 a₁ b₁ x / (3 * s ^ a₂ * x ^ (↑mu * a₂))

ε₂^{b₂} · 3 σ^{a₂} x^{μ a₂} = ε₁.

theorem MIPRE.Pipeline.ar_margin {a₁ b₁ a₂ b₂ : ℝ} {mu : ℕ} {s x : ℝ} (ha₁ : 1 ≤ a₁) (hb₂ : 0 < b₂) (hs : 0 < s) (hx : 0 < x) (hmargin : s ^ a₂ * x ^ (-(↑mu * b₂)) < eps1 a₁ b₁ x / 2) : s ^ a₂ * (x ^ (↑mu * a₂) * eps2 a₁ b₁ a₂ b₂ mu s x ^ b₂ + x ^ (-(↑mu * b₂))) < eps1 a₁ b₁ x

The answer-reduction step lands inside the introspection margin: with the margin claim, δ₂(ε₂, n) < ε₁.

theorem MIPRE.Pipeline.exists_eps2_lower {a₁ b₁ a₂ b₂ : ℝ} (ha₁ : 1 ≤ a₁) (hb₁ : 0 < b₁) (ha₂ : 1 ≤ a₂) (hb₂ : 0 < b₂) (mu K : ℕ) : ∃ (P : ℕ) (N : ℕ), ∀ (x : ℝ), ↑N ≤ x → ∀ (s : ℝ), 1 ≤ s → s ≤ x ^ ↑K → x ^ (-↑P) ≤ eps2 a₁ b₁ a₂ b₂ mu s x

1/ε₂ is a fixed power of x: x^{-P} ≤ ε₂ for a universal P and x past a threshold, whenever 1 ≤ σ ≤ x^K.

A universal repetition exponent

theorem MIPRE.Pipeline.exists_tau {c : ℝ} (hc : 0 < c) (P beta : ℕ) : ∃ (tau : ℕ), ∀ (z : ℝ), ↑tau ≤ z → ∀ (k : ℝ), z ^ tau ≤ k → ∀ (B : ℝ), 0 ≤ B → B ≤ z ^ beta → ∀ (ε : ℝ), 0 < ε → z ^ (-↑P) ≤ ε → Real.exp (-(c * ε ^ 13 * k / (B + 1))) ≤ 1 / 2

A universal repetition exponent (blueprint lem:compress-tau). For the constant c of repetition, a bound ε ≥ z^{-P} on the gap and an exponent β on the parse length, there is τ such that exp(-c ε^{13} k / (B + 1)) ≤ 1/2 for all z ≥ τ, k ≥ z^τ and 0 ≤ B ≤ z^β.