The compression theorem from its three stages

Blueprint thm:compression, its proof (paper recursive.tex, Section "Proof of Theorem compression"; ledger nodes 1.5, 1.5.7, 1.5.8): Compress is introspection at ℓ = 7, then answer reduction at (λ, μ, σ(λ)), then parallel repetition at (λ, τ, β), and its guarantees are those of the three stages chained through the margins of MIPRE.Foundations.Pipeline.Margin. GapCompression.ofPipeline is that composition: from an Introspection 7, an AnswerReduction 5 and a Repetition 7 it builds a GapCompression. Oracularization is not a stage of Compress (it is the first step of the proof of answer reduction) and is not consumed here.

The parameters, all determined by the three structures:

• σ(λ): the paper's ⌈C λ^C⌉, any polynomial in λ computable in polynomial time that dominates the size C(λ + 1)^C of the introspective decider and the size s₁(λ) of the introspective sampler — the second because answer reduction runs the input sampler through the universal machine, whose overhead grows with the program simulated, so its complexity clause asks |𝒮|, |𝒟| ≤ σ. It is sigmaFun C_σ λ, the C_σ-fold iterate of n ↦ 2^{2·size n} on 2λ + 1, which is 2^{C(size λ + 2)} at least and is computed by iterating lamProg; there is no polynomial-time arithmetic in the toolkit to compute the paper's expression directly, and any dominating polynomial serves.
• μ: the margin claim exists_mu, at least C + 1: at least C so that the introspective verifier is within answer reduction's input budget, and positive, as answer reduction's completeness asks.
• β: an exponent with poly((λn + 1)^μ + σ(λ) + λ + n)^(μ + 1) ≤ (λn + 1)^β, the parse length handed to repetition, dominating the ambient answer bound of the answer-reduced verifier.
• τ: the repetition exponent exists_tau, from the lower bound ε₂ ≥ x^{-P} of exists_eps2_lower, against the parse length 2^{β(|λ| + |n|)} ≤ (λn + 1)^{6β}.
• C₀: the largest of the thresholds — 2, the introspection margin's, the margin claim's, the lower bound's, answer reduction's own C_ar, and τ.

The complexity accounting is PolyBounded arithmetic: every bound of the repeated verifier at (λ, n) is a monotone polynomial expression in λ, n, σ(λ) and the sizes of the programs along the chain, hence at most a polynomial in n + λ (bound). The value chain is the one of rem:compression-chain: each soundness clause contrapositively, landing inside the margin the previous stage left.

The size parameter σ

noncomputable def MIPRE.Pipeline.twoPowFun : Cost.PolyTimeFun ℕ ℕ

n ↦ 2^{2·size n} as a polynomial-time function (lamProg).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Pipeline.sigmaFun : ℕ → Cost.PolyTimeFun ℕ ℕ

sigmaFun C: the C-fold iterate of n ↦ 2^{2·size n} on 2n + 1, a polynomial-time function of n bounded below by 2^{C(size n + 2)} and above by a polynomial in n.

Equations

• MIPRE.Pipeline.sigmaFun 0 = MIPRE.Cost.PolyTimeFun.next
• MIPRE.Pipeline.sigmaFun C.succ = MIPRE.Pipeline.twoPowFun.comp (MIPRE.Pipeline.sigmaFun C)

theorem MIPRE.Pipeline.sigmaFun_zero (n : ℕ) : (sigmaFun 0).toFun n = 2 * n + 1

theorem MIPRE.Pipeline.sigmaFun_succ (C n : ℕ) : (sigmaFun (C + 1)).toFun n = 2 ^ (2 * ((sigmaFun C).toFun n).size)

theorem MIPRE.Pipeline.size_sigmaFun (C n : ℕ) : C * (n.size + 2) + n.size + 1 ≤ ((sigmaFun C).toFun n).size

theorem MIPRE.Pipeline.one_le_sigmaFun (C n : ℕ) : 1 ≤ (sigmaFun C).toFun n

theorem MIPRE.Pipeline.le_sigmaFun (C n : ℕ) : C * (n + 1) ^ C ≤ (sigmaFun C).toFun n

C (n + 1)^C ≤ sigmaFun C n: the size of the introspective decider is dominated.

theorem MIPRE.Pipeline.sigmaFun_mono (C : ℕ) {m n : ℕ} (h : m ≤ n) : (sigmaFun C).toFun m ≤ (sigmaFun C).toFun n

theorem MIPRE.Pipeline.polyBounded_sigmaFun (C : ℕ) : Cost.PolyBounded (sigmaFun C).toFun

The parameters

noncomputable def MIPRE.Pipeline.s₁ (I : Introspection 7) (lam : ℕ) : ℕ

A bound on the size of the introspective sampler's program.

Equations

• MIPRE.Pipeline.s₁ I lam = Polynomial.eval (4 * lam.size + 1) I.samplerProg.timeBound

theorem MIPRE.Pipeline.sampler_size_le_s₁ (I : Introspection 7) (lam : ℕ) : (I.sampler lam).size ≤ s₁ I lam

noncomputable def MIPRE.Pipeline.cS (I : Introspection 7) : ℕ

The coefficient of the monomial bound on s₁.

Equations

• MIPRE.Pipeline.cS I = (∑ i ∈ Finset.range (I.samplerProg.timeBound.natDegree + 1), I.samplerProg.timeBound.coeff i) * 4 ^ I.samplerProg.timeBound.natDegree

theorem MIPRE.Pipeline.s₁_le (I : Introspection 7) (lam : ℕ) : s₁ I lam ≤ cS I * (lam + 1) ^ I.samplerProg.timeBound.natDegree

noncomputable def MIPRE.Pipeline.Csig (I : Introspection 7) : ℕ

The exponent of σ: large enough that C_σ (λ + 1)^{C_σ} dominates both the introspective decider's size C(λ + 1)^C and the introspective sampler's size s₁.

Equations

• MIPRE.Pipeline.Csig I = I.C + MIPRE.Pipeline.cS I + I.samplerProg.timeBound.natDegree

theorem MIPRE.Pipeline.mul_pow_le_Csig (I : Introspection 7) {c d : ℕ} (hc : c ≤ Csig I) (hd : d ≤ Csig I) (lam : ℕ) : c * (lam + 1) ^ d ≤ Csig I * (lam + 1) ^ Csig I

noncomputable def MIPRE.Pipeline.sigma (I : Introspection 7) (lam : ℕ) : ℕ

σ(λ) = sigmaFun C_σ λ.

Equations

• MIPRE.Pipeline.sigma I lam = (MIPRE.Pipeline.sigmaFun (MIPRE.Pipeline.Csig I)).toFun lam

theorem MIPRE.Pipeline.decider_size_le_sigma (I : Introspection 7) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (I.output V lam).decider.size ≤ sigma I lam

theorem MIPRE.Pipeline.sampler_size_le_sigma (I : Introspection 7) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (I.output V lam).sampler.size ≤ sigma I lam

theorem MIPRE.Pipeline.size_le_sigma (I : Introspection 7) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (I.output V lam).size ≤ sigma I lam

Both programs of the introspective verifier are within σ(λ).

theorem MIPRE.Pipeline.one_le_sigma (I : Introspection 7) (lam : ℕ) : 1 ≤ sigma I lam

theorem MIPRE.Pipeline.sigma_mono (I : Introspection 7) {m n : ℕ} (h : m ≤ n) : sigma I m ≤ sigma I n

noncomputable def MIPRE.Pipeline.K (I : Introspection 7) : ℕ

The exponent K with σ(z) ≤ z^K for z ≥ 2.

Equations

• MIPRE.Pipeline.K I = ⋯.choose

theorem MIPRE.Pipeline.sigma_le_pow (I : Introspection 7) (z : ℕ) : 2 ≤ z → sigma I z ≤ z ^ K I

noncomputable def MIPRE.Pipeline.mu (I : Introspection 7) (A : AnswerReduction 5) : ℕ

μ, from the margin claim.

Equations

• MIPRE.Pipeline.mu I A = ⋯.choose

theorem MIPRE.Pipeline.C_succ_le_mu (I : Introspection 7) (A : AnswerReduction 5) : I.C + 1 ≤ mu I A

theorem MIPRE.Pipeline.C_le_mu (I : Introspection 7) (A : AnswerReduction 5) : I.C ≤ mu I A

theorem MIPRE.Pipeline.one_le_mu (I : Introspection 7) (A : AnswerReduction 5) : 1 ≤ mu I A

μ ≥ 1, which answer reduction's completeness asks.

noncomputable def MIPRE.Pipeline.N₁ (I : Introspection 7) (A : AnswerReduction 5) : ℕ

The threshold of the margin claim.

Equations

• MIPRE.Pipeline.N₁ I A = ⋯.choose

theorem MIPRE.Pipeline.margin_spec (I : Introspection 7) (A : AnswerReduction 5) (x : ℝ) : ↑(N₁ I A) ≤ x → ∀ (s : ℝ), 1 ≤ s → s ≤ x ^ ↑(K I) → s ^ A.a * x ^ (-(↑(mu I A) * A.b)) < eps1 I.a I.b x / 2

theorem MIPRE.Pipeline.polyBounded_arBound (I : Introspection 7) (A : AnswerReduction 5) : Cost.PolyBounded fun (z : ℕ) => Polynomial.eval (z ^ mu I A + sigma I z + z + z) A.bound ^ (mu I A + 1)

noncomputable def MIPRE.Pipeline.beta (I : Introspection 7) (A : AnswerReduction 5) : ℕ

β, the parse-length exponent handed to repetition.

Equations

• MIPRE.Pipeline.beta I A = ⋯.choose

theorem MIPRE.Pipeline.arBound_le_pow (I : Introspection 7) (A : AnswerReduction 5) (z : ℕ) : 2 ≤ z → Polynomial.eval (z ^ mu I A + sigma I z + z + z) A.bound ^ (mu I A + 1) ≤ z ^ beta I A

noncomputable def MIPRE.Pipeline.P (I : Introspection 7) (A : AnswerReduction 5) : ℕ

P, with ε₂ ≥ x^{-P}.

Equations

• MIPRE.Pipeline.P I A = ⋯.choose

noncomputable def MIPRE.Pipeline.N₂ (I : Introspection 7) (A : AnswerReduction 5) : ℕ

The threshold of the lower bound on ε₂.

Equations

• MIPRE.Pipeline.N₂ I A = ⋯.choose

theorem MIPRE.Pipeline.eps2_lower_spec (I : Introspection 7) (A : AnswerReduction 5) (x : ℝ) : ↑(N₂ I A) ≤ x → ∀ (s : ℝ), 1 ≤ s → s ≤ x ^ ↑(K I) → x ^ (-↑(P I A)) ≤ eps2 I.a I.b A.a A.b (mu I A) s x

noncomputable def MIPRE.Pipeline.tau (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : ℕ

τ, the repetition exponent, against the parse length 2^{β(|λ| + |n|)} ≤ (λn + 1)^{6β}.

Equations

• MIPRE.Pipeline.tau I A R = ⋯.choose

theorem MIPRE.Pipeline.tau_spec (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (z : ℝ) : ↑(tau I A R) ≤ z → ∀ (k : ℝ), z ^ tau I A R ≤ k → ∀ (B : ℝ), 0 ≤ B → B ≤ z ^ (6 * beta I A) → ∀ (ε : ℝ), 0 < ε → z ^ (-↑(P I A)) ≤ ε → Real.exp (-(R.c * ε ^ 13 * k / (B + 1))) ≤ 1 / 2

theorem MIPRE.Pipeline.size_mul_add_one_le {lam n : ℕ} (hl : 1 ≤ lam) : (lam * n + 1).size ≤ lam.size + n.size

|λn + 1| ≤ |λ| + |n| for λ ≥ 1.

theorem MIPRE.Pipeline.pow_le_reps {lam n : ℕ} (hl : 1 ≤ lam) (tau : ℕ) : (lam * n + 1) ^ tau ≤ Repetition.reps lam tau n

(λn + 1)^τ ≤ k(n).

theorem MIPRE.Pipeline.parseBound_le {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (beta : ℕ) : Repetition.parseBound lam beta n ≤ (lam * n + 1) ^ (6 * beta)

B(n) ≤ (λn + 1)^{6β} for λ, n ≥ 1.

noncomputable def MIPRE.Pipeline.C₁ (I : Introspection 7) : ℕ

The threshold of the introspection margin, ⌈(4a)^{1/b}⌉.

Equations

• MIPRE.Pipeline.C₁ I = ⌈(4 * I.a) ^ (1 / I.b)⌉₊

noncomputable def MIPRE.Pipeline.C₀ (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : ℕ

C₀, the threshold of the compression theorem.

Equations

• MIPRE.Pipeline.C₀ I A R = max (max (max 2 (MIPRE.Pipeline.C₁ I)) (max (MIPRE.Pipeline.N₁ I A) (MIPRE.Pipeline.N₂ I A))) (max A.C (MIPRE.Pipeline.tau I A R))

theorem MIPRE.Pipeline.C₀_spec (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) {n : ℕ} (hn : C₀ I A R ≤ n) : 2 ≤ n ∧ C₁ I ≤ n ∧ N₁ I A ≤ n ∧ N₂ I A ≤ n ∧ A.C ≤ n ∧ tau I A R ≤ n

The data

noncomputable def MIPRE.Pipeline.arOutput (I : Introspection 7) (A : AnswerReduction 5) (V₁ : Verifier 5) (lam : ℕ) : Verifier 7

The answer-reduced verifier, at level 7 = max (5 + 2) 5.

Equations

• MIPRE.Pipeline.arOutput I A V₁ lam = A.output V₁ lam (MIPRE.Pipeline.mu I A) (MIPRE.Pipeline.sigma I lam)

noncomputable def MIPRE.Pipeline.arSampler (I : Introspection 7) (A : AnswerReduction 5) (S : CL.Sampler 5) (lam : ℕ) : CL.Sampler 7

The answer-reduced sampler, at level 7.

Equations

• MIPRE.Pipeline.arSampler I A S lam = A.sampler S lam (MIPRE.Pipeline.mu I A) (MIPRE.Pipeline.sigma I lam)

theorem MIPRE.Pipeline.arOutput_sampler (I : Introspection 7) (A : AnswerReduction 5) (V₁ : Verifier 5) (lam : ℕ) : (arOutput I A V₁ lam).sampler = arSampler I A V₁.sampler lam

theorem MIPRE.Pipeline.arSampler_prog (I : Introspection 7) (A : AnswerReduction 5) (S : CL.Sampler 5) (lam : ℕ) : A.samplerProg.toFun (S.prog, lam, mu I A, sigma I lam) = (arSampler I A S lam).prog

theorem MIPRE.Pipeline.arOutput_decider (I : Introspection 7) (A : AnswerReduction 5) (V₁ : Verifier 5) (lam : ℕ) : (arOutput I A V₁ lam).decider.prog = A.compute.toFun ((V₁.sampler.prog, V₁.decider.prog), lam, mu I A, sigma I lam)

noncomputable def MIPRE.Pipeline.sampler (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam : ℕ) : CL.Sampler 7

The compressed sampler 𝒮^compr_λ.

Equations

• MIPRE.Pipeline.sampler I A R lam = R.sampler (MIPRE.Pipeline.arSampler I A (I.sampler lam) lam) lam (MIPRE.Pipeline.tau I A R)

noncomputable def MIPRE.Pipeline.samplerProg (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : Cost.PolyTimeFun ℕ Cost.Prog

Its program, as a polynomial-time function of λ.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Pipeline.samplerProg_eq (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam : ℕ) : (samplerProg I A R).toFun lam = (sampler I A R lam).prog

noncomputable def MIPRE.Pipeline.compress (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × ℕ) Cost.Prog

Compress: the program of the compressed decider, as a polynomial-time function of the input programs and λ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Pipeline.output (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : Verifier 7

The output of Compress on any input, as a 7-level normal form verifier.

Equations

• MIPRE.Pipeline.output I A R V lam = R.output (MIPRE.Pipeline.arOutput I A (I.output V lam) lam) lam (MIPRE.Pipeline.tau I A R) (MIPRE.Pipeline.beta I A)

theorem MIPRE.Pipeline.output_sampler (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (output I A R V lam).sampler = sampler I A R lam

theorem MIPRE.Pipeline.output_decider (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (output I A R V lam).decider.prog = (compress I A R).toFun (V, lam)

The accounting

noncomputable def MIPRE.Pipeline.pArg (I : Introspection 7) (A : AnswerReduction 5) (lam : ℕ) : ℕ

A bound on the size of the encoded parameters (λ, μ, σ(λ)).

Equations

• MIPRE.Pipeline.pArg I A lam = 4 * lam.size + 1 + (MIPRE.Cost.esize (MIPRE.Pipeline.mu I A) + (4 * (MIPRE.Pipeline.sigma I lam).size + 1) + 1) + 1

theorem MIPRE.Pipeline.esize_params_le (I : Introspection 7) (A : AnswerReduction 5) (lam : ℕ) : Cost.esize (lam, mu I A, sigma I lam) ≤ pArg I A lam

noncomputable def MIPRE.Pipeline.wSize (I : Introspection 7) (A : AnswerReduction 5) (lam : ℕ) : ℕ

A bound on the size of the answer-reduced verifier, as a function of λ.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Pipeline.arOutput_size_le (I : Introspection 7) (A : AnswerReduction 5) (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (arOutput I A (I.output V lam) lam).size ≤ wSize I A lam

noncomputable def MIPRE.Pipeline.arBound (I : Introspection 7) (A : AnswerReduction 5) (lam n : ℕ) : ℕ

The bound of the answer-reduced verifier at (λ, n).

Equations

• MIPRE.Pipeline.arBound I A lam n = MIPRE.AnswerReduction.outBound A.bound lam (MIPRE.Pipeline.mu I A) (MIPRE.Pipeline.sigma I lam) n

noncomputable def MIPRE.Pipeline.arDegree (I : Introspection 7) (A : AnswerReduction 5) : ℕ

The answer-reduced verifier's input-size degree. The pipeline fixes μ, so this degree is independent of λ, n, and the input verifier.

Equations

• MIPRE.Pipeline.arDegree I A = MIPRE.AnswerReduction.outDegree A.deg (MIPRE.Pipeline.mu I A)

noncomputable def MIPRE.Pipeline.timeB (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam n : ℕ) : ℕ

The running-time bound of the compressed verifier at (λ, n).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Pipeline.ansB (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam n : ℕ) : ℕ

The answer bound of the compressed verifier at (λ, n).

Equations

• MIPRE.Pipeline.ansB I A R lam n = Polynomial.eval (MIPRE.Repetition.ansArg lam (MIPRE.Pipeline.tau I A R) (MIPRE.Pipeline.beta I A) n) R.ansBound

noncomputable def MIPRE.Pipeline.G (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (z : ℕ) : ℕ

Both bounds, as one function of z = n + λ.

Equations

• MIPRE.Pipeline.G I A R z = MIPRE.Pipeline.timeB I A R z z + MIPRE.Pipeline.ansB I A R z z

theorem MIPRE.Pipeline.timeB_mono (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) {lam n lam' n' : ℕ} (hl : lam ≤ lam') (hn : n ≤ n') : timeB I A R lam n ≤ timeB I A R lam' n'

theorem MIPRE.Pipeline.ansB_mono (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) {lam n lam' n' : ℕ} (hl : lam ≤ lam') (hn : n ≤ n') : ansB I A R lam n ≤ ansB I A R lam' n'

theorem MIPRE.Pipeline.timeB_le_G (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam n : ℕ) : timeB I A R lam n ≤ G I A R (n + lam)

theorem MIPRE.Pipeline.ansB_le_G (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam n : ℕ) : ansB I A R lam n ≤ G I A R (n + lam)

theorem MIPRE.Pipeline.polyBounded_G (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : Cost.PolyBounded (G I A R)

noncomputable def MIPRE.Pipeline.bound (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : Polynomial ℕ

The polynomial poly(n, λ) of the compression theorem.

Equations

• MIPRE.Pipeline.bound I A R = ⋯.poly

theorem MIPRE.Pipeline.timeB_le_bound (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam n : ℕ) : timeB I A R lam n ≤ Polynomial.eval (n + lam) (bound I A R)

theorem MIPRE.Pipeline.ansB_le_bound (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (lam n : ℕ) : ansB I A R lam n ≤ Polynomial.eval (n + lam) (bound I A R)

theorem MIPRE.Pipeline.introOutput_within (I : Introspection 7) (A : AnswerReduction 5) (V : Cost.Prog × Cost.Prog) (lam n : ℕ) : (I.output V lam).Within n (AnswerReduction.inBudget lam (mu I A) n)

The introspective verifier is within answer reduction's input budget.

theorem MIPRE.Pipeline.ansBound_le_inAns (I : Introspection 7) (A : AnswerReduction 5) (lam n : ℕ) : Introspection.ansBound I.C lam n ≤ AnswerReduction.inAns lam (mu I A) n

theorem MIPRE.Pipeline.arOutput_within (I : Introspection 7) (A : AnswerReduction 5) (V : Cost.Prog × Cost.Prog) (lam n : ℕ) : (arOutput I A (I.output V lam) lam).Within n (Budget.uniform (arBound I A lam n) (arDegree I A))

The answer-reduced verifier is within its bound.

theorem MIPRE.Pipeline.output_within (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (V : Cost.Prog × Cost.Prog) (lam n : ℕ) : (output I A R V lam).Within n { S := timeB I A R lam n, d := timeB I A R lam n, D := timeB I A R lam n, k := R.deg * (arDegree I A + 1), B := ansB I A R lam n }

The compressed verifier is within its bounds.

theorem MIPRE.Pipeline.arBound_le_parseBound (I : Introspection 7) (A : AnswerReduction 5) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) : arBound I A lam n ≤ Repetition.parseBound lam (beta I A) n

The answer bound of the answer-reduced verifier is below the parse length handed to repetition, for λ ≥ 1 and n ≥ 1.

The value chain

theorem MIPRE.Pipeline.output_hasPerfectPCC (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (V : Verifier 7) (lam n : ℕ) (hB : V.IsBounded lam) (hn : C₀ I A R ≤ n) (h : V.HasPerfectPCC (2 ^ n) ((2 ^ n) ^ lam)) : (output I A R (V.sampler.prog, V.decider.prog) lam).HasPerfectPCC n (ansB I A R lam n)

Completeness of Compress: the three completeness clauses chained.

theorem MIPRE.Pipeline.output_val_le (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (ω : ValueModel) (hI : I.SoundIn ω) (hA : A.SoundIn ω) (hR : R.SoundIn ω) (V : Verifier 7) (lam n : ℕ) (hB : V.IsBounded lam) (hn : C₀ I A R ≤ n) (h : V.val ω (2 ^ n) ((2 ^ n) ^ lam) ≤ 1 / 2) : (output I A R (V.sampler.prog, V.decider.prog) lam).val ω n (ansB I A R lam n) ≤ 1 / 2

Soundness of Compress in a value model, value form: the three stages' soundness clauses in the model, contrapositively, through the margins. The margins and the parameters are the same in every model; only the clauses are the model's.

theorem MIPRE.Pipeline.output_valStar_le (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) (V : Verifier 7) (lam n : ℕ) (hB : V.IsBounded lam) (hn : C₀ I A R ≤ n) (h : V.valStar (2 ^ n) ((2 ^ n) ^ lam) ≤ 1 / 2) : (output I A R (V.sampler.prog, V.decider.prog) lam).valStar n (ansB I A R lam n) ≤ 1 / 2

Soundness of Compress, value form: output_val_le in the tensor-product model, where the stages' own soundness fields are the clauses.

noncomputable def MIPRE.GapCompression.ofPipeline (I : Introspection 7) (A : AnswerReduction 5) (R : Repetition 7) : GapCompression

The compression theorem from its stages (blueprint thm:compression, proof): an Introspection 7, an AnswerReduction 5 and a Repetition 7 give a GapCompression.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.GapCompression.ofPipeline_sound {I : Introspection 7} {A : AnswerReduction 5} {R : Repetition 7} {ω : ValueModel} (hI : I.SoundIn ω) (hA : A.SoundIn ω) (hR : R.SoundIn ω) : (ofPipeline I A R).Sound ω

The composed compression is sound in every value model in which its three stages are (item (c) of Phase 1 of planning/mipco-track.md). In the tensor-product model the stages' own fields are the three clauses, and this is GapCompression.sound_tensor; in the commuting-operator model it reduces the one hypothesis of the conditional MIP^co = coRE to the three stages' clauses in ω_co.