Tailored compression from its three stages

Phase 5 of planning/aldous-lyons-track.md; paper II, thm:h_level_compression (II:5643), in value form. TailoredGapCompression.ofTailoredPipeline composes question reduction (TailoredIntrospection 7), answer reduction (TailoredAnswerReduction 5) and parallel repetition (TailoredRepetition 7) into a TailoredGapCompression 7, along the route of the existing pipeline's GapCompression.ofPipeline (MIPRE/Foundations/Pipeline/Compress.lean), whose margins (MIPRE/Foundations/Pipeline/Margin.lean) it reuses.

What differs from the existing composition:

• every verifier has three programs, so the size parameter σ(λ) dominates the sizes of the introspective sampler, answer-length calculator and linear-constraints processor, and the accounting carries a third program in every line;
• the compressed answer-length calculator depends on λ only: it is repetition's calculator on the answer-reduced sampler and calculator at λ, which depend on λ only;
• completeness is read in perfect ZPC strategies, and the chain has no answer bounds to adjust;
• repetition reads its input's lengths from the calculator, so the parse exponent β becomes an exponent bounding the answer-reduced lengths, B(λ, n) ≤ (λn + 1)^β, which τ is chosen against.

theorem MIPRE.Tailored.TailoredVerifier.Within.mono {ℓ : ℕ} {V : TailoredVerifier ℓ} {n : ℕ} {R R' : Budget} (h : V.Within n R) (hle : R.Le R') : V.Within n R'

The size of a program computed from λ

noncomputable def MIPRE.Tailored.Compose.coefOf (f : Cost.PolyTimeFun ℕ Cost.Prog) : ℕ

The coefficient of the monomial bound on the size of f λ.

Equations

• MIPRE.Tailored.Compose.coefOf f = (∑ i ∈ Finset.range (f.timeBound.natDegree + 1), f.timeBound.coeff i) * 4 ^ f.timeBound.natDegree

theorem MIPRE.Tailored.Compose.esize_le_coefOf (f : Cost.PolyTimeFun ℕ Cost.Prog) (lam : ℕ) : Cost.esize (f.toFun lam) ≤ coefOf f * (lam + 1) ^ f.timeBound.natDegree

|f λ| ≤ c (λ + 1)^d for a polynomial-time f.

noncomputable def MIPRE.Tailored.Compose.sizeOf (f : Cost.PolyTimeFun ℕ Cost.Prog) (lam : ℕ) : ℕ

|f λ| ≤ poly(|λ|), the bound monotone in λ.

Equations

• MIPRE.Tailored.Compose.sizeOf f lam = Polynomial.eval (4 * lam.size + 1) f.timeBound

theorem MIPRE.Tailored.Compose.esize_le_sizeOf (f : Cost.PolyTimeFun ℕ Cost.Prog) (lam : ℕ) : Cost.esize (f.toFun lam) ≤ sizeOf f lam

theorem MIPRE.Tailored.Compose.polyBounded_sizeOf (f : Cost.PolyTimeFun ℕ Cost.Prog) : Cost.PolyBounded (sizeOf f)

The parameters

noncomputable def MIPRE.Tailored.Compose.Csig (I : TailoredIntrospection 7) : ℕ

The exponent of σ: C_σ (λ + 1)^{C_σ} dominates the sizes of the three introspective programs.

Equations

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

theorem MIPRE.Tailored.Compose.mul_pow_le_Csig (I : TailoredIntrospection 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.Tailored.Compose.sigma (I : TailoredIntrospection 7) (lam : ℕ) : ℕ

σ(λ).

Equations

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

theorem MIPRE.Tailored.Compose.le_sigma (I : TailoredIntrospection 7) {c d : ℕ} (hc : c ≤ Csig I) (hd : d ≤ Csig I) (lam : ℕ) : c * (lam + 1) ^ d ≤ sigma I lam

theorem MIPRE.Tailored.Compose.size_le_sigma (I : TailoredIntrospection 7) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (I.output V lam).size ≤ sigma I lam

The introspective verifier is within σ(λ): all three of its programs.

theorem MIPRE.Tailored.Compose.one_le_sigma (I : TailoredIntrospection 7) (lam : ℕ) : 1 ≤ sigma I lam

theorem MIPRE.Tailored.Compose.sigma_mono (I : TailoredIntrospection 7) {m n : ℕ} (h : m ≤ n) : sigma I m ≤ sigma I n

noncomputable def MIPRE.Tailored.Compose.K (I : TailoredIntrospection 7) : ℕ

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

Equations

• MIPRE.Tailored.Compose.K I = ⋯.choose

theorem MIPRE.Tailored.Compose.sigma_le_pow (I : TailoredIntrospection 7) (z : ℕ) : 2 ≤ z → sigma I z ≤ z ^ K I

noncomputable def MIPRE.Tailored.Compose.mu (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : ℕ

μ, from the margin claim, at least C + 1.

Equations

• MIPRE.Tailored.Compose.mu I A = ⋯.choose

theorem MIPRE.Tailored.Compose.C_succ_le_mu (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : I.C + 1 ≤ mu I A

theorem MIPRE.Tailored.Compose.C_le_mu (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : I.C ≤ mu I A

theorem MIPRE.Tailored.Compose.one_le_mu (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : 1 ≤ mu I A

noncomputable def MIPRE.Tailored.Compose.N₁ (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : ℕ

The threshold of the margin claim.

Equations

• MIPRE.Tailored.Compose.N₁ I A = ⋯.choose

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

theorem MIPRE.Tailored.Compose.polyBounded_arBound (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 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.Tailored.Compose.beta (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : ℕ

β, an exponent bounding the answer-reduced lengths: B(λ, n) ≤ (λn + 1)^β.

Equations

• MIPRE.Tailored.Compose.beta I A = ⋯.choose

theorem MIPRE.Tailored.Compose.arBound_le_pow (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 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.Tailored.Compose.P (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : ℕ

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

Equations

• MIPRE.Tailored.Compose.P I A = ⋯.choose

noncomputable def MIPRE.Tailored.Compose.N₂ (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : ℕ

The threshold of the lower bound on ε₂.

Equations

• MIPRE.Tailored.Compose.N₂ I A = ⋯.choose

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

noncomputable def MIPRE.Tailored.Compose.tau (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) : ℕ

τ, the repetition exponent, against the lengths B(λ, n) ≤ (λn + 1)^β.

Equations

• MIPRE.Tailored.Compose.tau I A R = ⋯.choose

theorem MIPRE.Tailored.Compose.tau_spec (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (z : ℝ) : ↑(tau I A R) ≤ z → ∀ (k : ℝ), z ^ tau I A R ≤ k → ∀ (B : ℝ), 0 ≤ B → B ≤ z ^ beta I A → ∀ (ε : ℝ), 0 < ε → z ^ (-↑(P I A)) ≤ ε → Real.exp (-(R.c * ε ^ 13 * k / (B + 1))) ≤ 1 / 2

noncomputable def MIPRE.Tailored.Compose.C₁ (I : TailoredIntrospection 7) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Compose.C₀ (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) : ℕ

C₀, the threshold of the compression theorem.

Equations

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

theorem MIPRE.Tailored.Compose.C₀_spec (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 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.Tailored.Compose.arOutput (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : TailoredVerifier 7

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

Equations

• MIPRE.Tailored.Compose.arOutput I A V lam = A.output (I.output V lam) lam (MIPRE.Tailored.Compose.mu I A) (MIPRE.Tailored.Compose.sigma I lam)

noncomputable def MIPRE.Tailored.Compose.arSampler (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : CL.Sampler 7

The answer-reduced sampler at λ, which depends on λ only.

Equations

• MIPRE.Tailored.Compose.arSampler I A lam = A.sampler (I.sampler lam) lam (MIPRE.Tailored.Compose.mu I A) (MIPRE.Tailored.Compose.sigma I lam)

noncomputable def MIPRE.Tailored.Compose.arLen (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : Decider

The answer-reduced calculator at λ.

Equations

• MIPRE.Tailored.Compose.arLen I A lam = A.len lam (MIPRE.Tailored.Compose.mu I A) (MIPRE.Tailored.Compose.sigma I lam)

theorem MIPRE.Tailored.Compose.arOutput_sampler (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (arOutput I A V lam).sampler = arSampler I A lam

theorem MIPRE.Tailored.Compose.arOutput_len (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (arOutput I A V lam).len = arLen I A lam

noncomputable def MIPRE.Tailored.Compose.paramsF (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : Cost.PolyTimeFun ℕ (ℕ × ℕ × ℕ)

The parameters (λ, μ, σ(λ)), as a polynomial-time function of λ.

Equations

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

theorem MIPRE.Tailored.Compose.paramsF_apply (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : (paramsF I A).toFun lam = (lam, mu I A, sigma I lam)

noncomputable def MIPRE.Tailored.Compose.arSamplerProg (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : Cost.PolyTimeFun ℕ Cost.Prog

The answer-reduced sampler's program, from λ.

Equations

• MIPRE.Tailored.Compose.arSamplerProg I A = A.samplerProg.comp (I.samplerProg.pair (MIPRE.Tailored.Compose.paramsF I A))

theorem MIPRE.Tailored.Compose.arSamplerProg_eq (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : (arSamplerProg I A).toFun lam = (arSampler I A lam).prog

noncomputable def MIPRE.Tailored.Compose.arLenProg (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : Cost.PolyTimeFun ℕ Cost.Prog

The answer-reduced calculator's program, from λ.

Equations

• MIPRE.Tailored.Compose.arLenProg I A = A.lenProg.comp (MIPRE.Tailored.Compose.paramsF I A)

theorem MIPRE.Tailored.Compose.arLenProg_eq (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : (arLenProg I A).toFun lam = (arLen I A lam).prog

noncomputable def MIPRE.Tailored.Compose.sampler (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam : ℕ) : CL.Sampler 7

The compressed sampler S^λ.

Equations

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

noncomputable def MIPRE.Tailored.Compose.samplerProg (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 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.Tailored.Compose.samplerProg_eq (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam : ℕ) : (samplerProg I A R).toFun lam = (sampler I A R lam).prog

noncomputable def MIPRE.Tailored.Compose.len (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam : ℕ) : Decider

The compressed answer-length calculator L^λ.

Equations

• MIPRE.Tailored.Compose.len I A R lam = R.len (MIPRE.Tailored.Compose.arSampler I A lam) (MIPRE.Tailored.Compose.arLen I A lam) lam (MIPRE.Tailored.Compose.tau I A R)

noncomputable def MIPRE.Tailored.Compose.lenProg (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 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.Tailored.Compose.lenProg_eq (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam : ℕ) : (lenProg I A R).toFun lam = (len I A R lam).prog

noncomputable def MIPRE.Tailored.Compose.compress (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog × Cost.Prog) × ℕ) Cost.Prog

Compress: the program of the compressed linear-constraints processor, from the input's three programs and λ.

Equations

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

noncomputable def MIPRE.Tailored.Compose.output (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : TailoredVerifier 7

The output of Compress.

Equations

• MIPRE.Tailored.Compose.output I A R V lam = R.output (MIPRE.Tailored.Compose.arOutput I A V lam) lam (MIPRE.Tailored.Compose.tau I A R)

theorem MIPRE.Tailored.Compose.output_sampler (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (output I A R V lam).sampler = sampler I A R lam

theorem MIPRE.Tailored.Compose.output_len (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (output I A R V lam).len = len I A R lam

theorem MIPRE.Tailored.Compose.arOutput_progs (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (arOutput I A V lam).progs = ((arSamplerProg I A).toFun lam, (arLenProg I A).toFun lam, A.compute.toFun ((I.samplerProg.toFun lam, I.lenProg.toFun lam, I.compute.toFun (V, lam)), lam, mu I A, sigma I lam))

theorem MIPRE.Tailored.Compose.output_lp (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (output I A R V lam).lp.prog = (compress I A R).toFun (V, lam)

The accounting

noncomputable def MIPRE.Tailored.Compose.pArg (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : ℕ

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

Equations

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

theorem MIPRE.Tailored.Compose.esize_params_le (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam : ℕ) : Cost.esize (lam, mu I A, sigma I lam) ≤ pArg I A lam

noncomputable def MIPRE.Tailored.Compose.wSize (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 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.Tailored.Compose.arOutput_size_le (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) : (arOutput I A V lam).size ≤ wSize I A lam

noncomputable def MIPRE.Tailored.Compose.arBound (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (lam n : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Compose.arDegree (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) : ℕ

The answer-reduced verifier's input-size degree.

Equations

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

noncomputable def MIPRE.Tailored.Compose.timeB (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 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.Tailored.Compose.lenB (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam n : ℕ) : ℕ

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

Equations

• MIPRE.Tailored.Compose.lenB I A R lam n = MIPRE.Repetition.reps lam (MIPRE.Tailored.Compose.tau I A R) n * MIPRE.Tailored.Compose.arBound I A lam n

noncomputable def MIPRE.Tailored.Compose.G (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (z : ℕ) : ℕ

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

Equations

• MIPRE.Tailored.Compose.G I A R z = MIPRE.Tailored.Compose.timeB I A R z z + MIPRE.Tailored.Compose.lenB I A R z z

theorem MIPRE.Tailored.Compose.arBound_mono (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) {lam n lam' n' : ℕ} (hl : lam ≤ lam') (hn : n ≤ n') : arBound I A lam n ≤ arBound I A lam' n'

theorem MIPRE.Tailored.Compose.timeB_mono (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 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.Tailored.Compose.lenB_mono (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) {lam n lam' n' : ℕ} (hl : lam ≤ lam') (hn : n ≤ n') : lenB I A R lam n ≤ lenB I A R lam' n'

theorem MIPRE.Tailored.Compose.timeB_le_G (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam n : ℕ) : timeB I A R lam n ≤ G I A R (n + lam)

theorem MIPRE.Tailored.Compose.lenB_le_G (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam n : ℕ) : lenB I A R lam n ≤ G I A R (n + lam)

theorem MIPRE.Tailored.Compose.polyBounded_G (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) : Cost.PolyBounded (G I A R)

noncomputable def MIPRE.Tailored.Compose.bound (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) : Polynomial ℕ

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

Equations

• MIPRE.Tailored.Compose.bound I A R = ⋯.poly

theorem MIPRE.Tailored.Compose.timeB_le_bound (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam n : ℕ) : timeB I A R lam n ≤ Polynomial.eval (n + lam) (bound I A R)

theorem MIPRE.Tailored.Compose.lenB_le_bound (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (lam n : ℕ) : lenB I A R lam n ≤ Polynomial.eval (n + lam) (bound I A R)

theorem MIPRE.Tailored.Compose.introOutput_within (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × 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.Tailored.Compose.arOutput_within (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam n : ℕ) : (arOutput I A V lam).Within n (Budget.uniform (arBound I A lam n) (arDegree I A))

The answer-reduced verifier is within its bound.

theorem MIPRE.Tailored.Compose.output_within (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : Cost.Prog × 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 := lenB I A R lam n }

The compressed verifier is within its bounds.

theorem MIPRE.Tailored.Compose.arBound_le_pow' (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) : arBound I A lam n ≤ (lam * n + 1) ^ beta I A

(λn + 1)^τ ≤ k(n), and the answer-reduced lengths are at most (λn + 1)^β.

The value chain

theorem MIPRE.Tailored.Compose.one_le_of_isBounded {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam : ℕ} (hB : V.IsBounded lam) : 1 ≤ lam

theorem MIPRE.Tailored.Compose.output_hasPerfectZPC (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : TailoredVerifier 7) (lam n : ℕ) (hB : V.IsBounded lam) (hn : C₀ I A R ≤ n) (h : V.HasPerfectZPC (2 ^ n)) : (output I A R V.progs lam).HasPerfectZPC n

Completeness of Compress: the three completeness clauses chained.

theorem MIPRE.Tailored.Compose.output_valStar_le (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) (V : TailoredVerifier 7) (lam n : ℕ) (hB : V.IsBounded lam) (hn : C₀ I A R ≤ n) (h : V.valStar (2 ^ n) ≤ 1 / 2) : (output I A R V.progs lam).valStar n ≤ 1 / 2

Soundness of Compress, value form: the three soundness clauses, contrapositively, through the margins.

noncomputable def MIPRE.Tailored.TailoredGapCompression.ofTailoredPipeline (I : TailoredIntrospection 7) (A : TailoredAnswerReduction 5) (R : TailoredRepetition 7) : TailoredGapCompression 7

Tailored compression from its stages (paper II, thm:h_level_compression, II:5643, value form): a TailoredIntrospection 7, a TailoredAnswerReduction 5 and a TailoredRepetition 7 give a TailoredGapCompression 7.

Equations

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