RE ⊆ MIP*_{1,1/2}(2,1), and MIP*_{1,1/2}(2,1) = RE

The class verifier of Paper/ClassVerifier.lean is a PolyVerifier for the polynomial classP chosen above its four cost bounds (sampB, dimB, decB, cutB, each polynomially bounded here), and:

• it is efficient on every input (classV_efficient): the sampler's cost and the decider's are within the polynomial, the questions have the compressed sampler's dimension at the fixed level, and the decider rejects overlong messages — the answers by its cutoff, the questions by the wrapper's length check;
• its game on z has the value of 𝒱^halt (R z) λ(z) at the fixed level C with the answers cut at cutz z (classV_value): the uniform seed of length B ≥ s(C) pushes forward, through its first s(C) bits, to the compressed sampler's distribution (SamplerFamily.game_μ_qEmb, SamplerFamily.game_support, in Paper/ClassSampler.lean), so the game is the restriction of the verifier's to the questions of length s(C) (quantumValue_restrictQuestions) with the answers extended by always-rejected ones (quantumValue_extendAnswers);
• that value is 1 on L and at most 1/2 off it (thm:halting at the fixed level, halting_paper): the cutoff is at least the compressor's answer bound, and below it the decider of 𝒱^halt rejects overlong answers whenever M does not halt.

Hence re_subset_mipstar_of and mipstar_eq_re_of (blueprint thm:mipstar-eq-re, for the paper's class), given a compressor and the two universal machines; the unconditional forms are in MIPRE/Background/Pipeline.lean and MIPRE/MainTheorem.lean.

The bounds are polynomial

theorem MIPRE.Halting.polyBounded_dimB (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (dimB G Λ₀ R)

theorem MIPRE.Halting.polyBounded_sampB (G : GapCompression) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (sampB G U Λ₀ R)

theorem MIPRE.Halting.polyBounded_TDB (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (TDB G U UT Λ₀ K R)

theorem MIPRE.Halting.polyBounded_zB (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (zB G Λ₀ R)

theorem MIPRE.Halting.polyBounded_decB (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (decB G U UT Λ₀ K R)

noncomputable def MIPRE.Halting.cutB (G : GapCompression) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The cutoff, in the input length.

Equations

• MIPRE.Halting.cutB G Λ₀ K R m = 2 ^ (K + G.bound.natDegree) * (2 * MIPRE.Halting.lamB Λ₀ R m + 1) ^ (4 * G.bound.natDegree)

theorem MIPRE.Halting.polyBounded_cutB (G : GapCompression) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (cutB G Λ₀ K R)

theorem MIPRE.Halting.cutz_le (G : GapCompression) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : cutz G Λ₀ K R z ≤ cutB G Λ₀ K R (List.length z)

The class verifier

noncomputable def MIPRE.Halting.classP (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Polynomial ℕ

The polynomial of the class verifier: above the sampler's cost, the dimension, the decider's cost and the cutoff.

Equations

• MIPRE.Halting.classP G U UT Λ₀ K R = ⋯.poly + ⋯.poly + ⋯.poly + ⋯.poly

theorem MIPRE.Halting.sampB_le (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : sampB G U Λ₀ R m ≤ Polynomial.eval m (classP G U UT Λ₀ K R)

theorem MIPRE.Halting.dimB_le (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : dimB G Λ₀ R m ≤ Polynomial.eval m (classP G U UT Λ₀ K R)

theorem MIPRE.Halting.decB_le (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : decB G U UT Λ₀ K R m ≤ Polynomial.eval m (classP G U UT Λ₀ K R)

theorem MIPRE.Halting.cutB_le (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : cutB G Λ₀ K R m ≤ Polynomial.eval m (classP G U UT Λ₀ K R)

noncomputable def MIPRE.Halting.classV (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : PolyVerifier

The class verifier of the language reduced to halting by R.

Equations

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

theorem MIPRE.Halting.dimz_le_B (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : dimz G Λ₀ R z ≤ (classV G U UT Λ₀ K R).B z

theorem MIPRE.Halting.cutz_le_B (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : cutz G Λ₀ K R z ≤ (classV G U UT Λ₀ K R).B z

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.Vz (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : Verifier 7

The verifier 𝒱^halt (R z) λ(z) the class verifier plays on z.

Equations

• MIPRE.Halting.Vz G U UT Λ₀ R z = MIPRE.Halting.Vpaper G U UT (R.toFun z) (MIPRE.Halting.lamz Λ₀ R z)

theorem MIPRE.Halting.classV_samples (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : G.samplerFamily.Samples (C G) Λ₀ R (classV G U UT Λ₀ K R)

The class verifier samples the compressed samplers at the fixed level.

theorem MIPRE.Halting.classV_efficient (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : (classV G U UT Λ₀ K R).Efficient z

The class verifier is efficient on every input.

The value of the game

theorem MIPRE.Halting.classV_value (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : quantumValue ((classV G U UT Λ₀ K R).game z) = (Vz G U UT Λ₀ R z).valStar (C G) (cutz G Λ₀ K R z)

The value of the class verifier's game is that of 𝒱^halt (R z) λ(z) at the fixed level C, with the answers cut at cutz z.

RE ⊆ MIP*, and MIP* = RE

theorem MIPRE.Halting.classV_values (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (hK : ∀ (lam : ℕ), Polynomial.eval (C G + lam) G.bound ≤ 2 ^ (K + G.bound.natDegree * Cost.esize lam)) (z : Cost.BitStr) : (Cost.Halts (R.toFun z) Cost.Data.nil → quantumValue ((classV G U UT (lamThreshold G U UT) K R).game z) = 1) ∧ (¬Cost.Halts (R.toFun z) Cost.Data.nil → quantumValue ((classV G U UT (lamThreshold G U UT) K R).game z) ≤ 1 / 2)

The values on and off the language, for the parameter Λ₀ of lem:lambda and a cutoff above the compressor's bound.

theorem MIPRE.Halting.re_subset_mipstar_of (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {L : Set Cost.BitStr} (hL : IsRE L) : MIPStar L

RE ⊆ MIP*_{1,1/2}(2,1), given a compressor and the two universal machines.

theorem MIPRE.Halting.mipstar_eq_re_of (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) : MIPStar = IsRE

MIP*_{1,1/2}(2,1) = RE (blueprint thm:mipstar-eq-re, the paper's class), given a compressor and the two universal machines.