RE ⊆ TMIP*, and TMIP* = RE, for the polynomial-time class

The polynomial-time tailored verifier (TPolyVerifier, Tailored/ClassPoly.lean) that puts an r.e. language L in the paper's class TMIP* (II:787), for a polynomial-time reduction R of L to halting on the empty input (Cost.exists_polyTime_reduction): on the input z it plays the game of the tailored halting verifier V^{R z, λ(z)} (Halting.VT) at the fixed level C, with λ(z) = Λ₀ + 4|R z| and Λ₀ the threshold of lem:lambda (Halting.lamThreshold).

• The sampler is the class sampler of Paper/ClassSampler.lean for the compressed samplers (TailoredGapCompression.samplerFamily) at the level C; at the level 0 of the compression it outputs the empty pair, the questions being empty there.
• The answer-length calculator, on (z, x, κ), computes the compressed calculator's program L^{λ(z)} (lenPrep) and runs it on (C, x, κ) through the universal machine.
• The linear-constraints processor, on (z, x, y, a^R, b^R), computes the program of the processor LP^{R z, λ(z)} of the halting verifier, in polynomial time (lpBuild, lpPrep), and runs it on (C, x, y, a^R, b^R) through the universal machine.

The universal machine's simulation halts exactly when the simulated program does, with its output (seqUniv_runs, seqUniv_runs_rev), so the calculator and the processor output what those of V^{R z, λ(z)} output at the level C (lenIs_iff, lpIs_iff). The game of the class verifier on z therefore extends that of V^{R z, λ(z)} at C along the embedding of the questions as bit strings (tgame_extends, TailoredGame.Extends): it has the same quantum value and inherits its perfect ZPC strategies, on the doubled games.

Efficiency (classTV_efficient). The sampler is Paper/ClassSampler.lean's. The compressed calculator runs within poly(C, λ(z)) times a power of its input's size (the field len_time of the compression), and the processor of V^{M,λ} within Q(C + |M| + λ) times one (exists_lp_cost_poly), so both class programs run within polynomials in the total input length (lenB, lpB), below the verifier's polynomial classTP.

Hence MIPRE.Tailored.re_subset_tmipStar_of from thm:tailored-halting at the fixed level (Halting.halting_tailored_search), and MIPRE.Tailored.tmipStar_eq_re_of with TMIPStar.isRE (Tailored/ClassPolyTab.lean).

def MIPRE.Tailored.TailoredGapCompression.samplerFamily {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : Halting.SamplerFamily ℓ

The compressed samplers of a tailored gap compression, as a polynomial-time family of samplers at its level.

Equations

• TG.samplerFamily = { sampler := TG.sampler, samplerProg := TG.samplerProg, samplerProg_eq := ⋯, bound := TG.bound, deg := TG.deg, sampler_time := ⋯, sampler_dim := ⋯ }

A preparation followed by the universal machine

theorem MIPRE.Tailored.seqUniv_runs (U : Cost.UniversalMachine) {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (P : Cost.PolyTimeFun α (Cost.Prog × β)) (a : α) {r : Cost.Data} {t : ℕ} (h : (P.toFun a).1.Runs (Cost.encode (P.toFun a).2) r t) : ∃ t' ≤ 2 * Polynomial.eval (Cost.esize a) P.timeBound + Polynomial.eval (Polynomial.eval (Cost.esize a) P.timeBound + t) U.bound + 3, (P.code.seq U.univ).Runs (Cost.encode a) r t'

A preparation followed by the universal machine runs the prepared program on the prepared input, at the cost of the preparation and of the simulation.

theorem MIPRE.Tailored.seqUniv_runs_rev (U : Cost.UniversalMachine) {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (P : Cost.PolyTimeFun α (Cost.Prog × β)) (a : α) {r : Cost.Data} {t : ℕ} (h : (P.code.seq U.univ).Runs (Cost.encode a) r t) : ∃ (t' : ℕ), (P.toFun a).1.Runs (Cost.encode (P.toFun a).2) r t'

It halts only if the prepared program does, with the same output.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Halting.VTz {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : TailoredVerifier ℓ

The tailored halting verifier the class verifier plays on z: V^{R z, λ(z)}.

Equations

• MIPRE.Tailored.Halting.VTz TG U UT Λ₀ R z = MIPRE.Tailored.Halting.VT TG U UT (R.toFun z) (MIPRE.Halting.lamz Λ₀ R z)

The calculator and the processor

noncomputable def MIPRE.Tailored.Halting.lenPrep {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Bool) (Cost.Prog × ℕ × Cost.BitStr × Bool)

The calculator's preparation: (z, x, κ) ↦ (L^{λ(z)}, (C, x, κ)).

Equations

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

theorem MIPRE.Tailored.Halting.lenPrep_apply {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x : Cost.BitStr) (κ : Bool) : (lenPrep TG Λ₀ R).toFun (z, x, κ) = ((TG.len (Halting.lamz Λ₀ R z)).prog, C TG, x, κ)

noncomputable def MIPRE.Tailored.Halting.lpPrep {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (Cost.Prog × ℕ × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr)

The processor's preparation: (z, x, y, a^R, b^R) ↦ (LP^{R z, λ(z)}, (C, x, y, a^R, b^R)).

Equations

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

theorem MIPRE.Tailored.Halting.lpPrep_apply {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y aR bR : Cost.BitStr) : (lpPrep TG U UT Λ₀ R).toFun (z, x, y, aR, bR) = ((VTz TG U UT Λ₀ R z).lp.prog, C TG, x, y, aR, bR)

The costs

noncomputable def MIPRE.Tailored.Halting.lenTB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The calculator's preparation time, in the total input length m.

Equations

• MIPRE.Tailored.Halting.lenTB TG Λ₀ R m = Polynomial.eval (4 * m + 7) (MIPRE.Tailored.Halting.lenPrep TG Λ₀ R).timeBound

noncomputable def MIPRE.Tailored.Halting.lenSB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The compressed calculator's time, in m.

Equations

• MIPRE.Tailored.Halting.lenSB TG Λ₀ R m = Polynomial.eval (MIPRE.Tailored.Halting.C TG + MIPRE.Halting.lamB Λ₀ R m) TG.bound * (4 * m + 6) ^ TG.deg

noncomputable def MIPRE.Tailored.Halting.lenB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The class calculator's cost, in the total input length.

Equations

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

noncomputable def MIPRE.Tailored.Halting.lpQ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) : Polynomial ℕ

The polynomial of the processor's cost (exists_lp_cost_poly).

Equations

• MIPRE.Tailored.Halting.lpQ TG U UT = ⋯.choose

noncomputable def MIPRE.Tailored.Halting.lpK {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) : ℕ

The degree of the processor's cost in the size of its input.

Equations

• MIPRE.Tailored.Halting.lpK TG U UT = ⋯.choose

theorem MIPRE.Tailored.Halting.lpQ_spec {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (lam n : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ Polynomial.eval (n + Cost.esize M + lam) (lpQ TG U UT) * (d.size + 1) ^ lpK TG U UT, (lpProg TG U UT (search TG) M lam).Runs ((Cost.encode n).cons d) r t

noncomputable def MIPRE.Tailored.Halting.lpTB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The processor's preparation time, in the total input length m.

Equations

• MIPRE.Tailored.Halting.lpTB TG U UT Λ₀ R m = Polynomial.eval (4 * m + 9) (MIPRE.Tailored.Halting.lpPrep TG U UT Λ₀ R).timeBound

noncomputable def MIPRE.Tailored.Halting.lpSB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The processor's time, in m.

Equations

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

noncomputable def MIPRE.Tailored.Halting.lpB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The class processor's cost, in the total input length.

Equations

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

theorem MIPRE.Tailored.Halting.polyBounded_lenB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (lenB TG U Λ₀ R)

theorem MIPRE.Tailored.Halting.polyBounded_lpB {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (lpB TG U UT Λ₀ R)

The class verifier

noncomputable def MIPRE.Tailored.Halting.classTP {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Polynomial ℕ

The polynomial of the class verifier: above the sampler's cost, the dimension, and the calculator's and the processor's costs.

Equations

• MIPRE.Tailored.Halting.classTP TG U UT Λ₀ R = ⋯.poly + ⋯.poly + ⋯.poly + ⋯.poly

theorem MIPRE.Tailored.Halting.classB_le {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : TG.samplerFamily.classB (C TG) U Λ₀ R m ≤ Polynomial.eval m (classTP TG U UT Λ₀ R)

theorem MIPRE.Tailored.Halting.dimB_le {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : TG.samplerFamily.dimB (C TG) Λ₀ R m ≤ Polynomial.eval m (classTP TG U UT Λ₀ R)

theorem MIPRE.Tailored.Halting.lenB_le {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : lenB TG U Λ₀ R m ≤ Polynomial.eval m (classTP TG U UT Λ₀ R)

theorem MIPRE.Tailored.Halting.lpB_le {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : lpB TG U UT Λ₀ R m ≤ Polynomial.eval m (classTP TG U UT Λ₀ R)

noncomputable def MIPRE.Tailored.Halting.classTV {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : TPolyVerifier

The polynomial-time tailored verifier of the language reduced to halting by R.

Equations

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

theorem MIPRE.Tailored.Halting.classTV_samples {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : TG.samplerFamily.Samples (C TG) Λ₀ R (classTV TG U UT Λ₀ R).toPoly

Its sampler samples the compressed samplers at the level C.

Efficiency

theorem MIPRE.Tailored.Halting.len_haltsWithin {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x : Cost.BitStr) (κ : Bool) : Cost.HaltsWithin (classTV TG U UT Λ₀ R).len (Cost.encode (z, x, κ)) (lenB TG U Λ₀ R (List.length z + List.length x))

The calculator halts within lenB of the total input length.

theorem MIPRE.Tailored.Halting.lp_haltsWithin {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y aR bR : Cost.BitStr) : Cost.HaltsWithin (classTV TG U UT Λ₀ R).lp (Cost.encode (z, x, y, aR, bR)) (lpB TG U UT Λ₀ R (List.length z + List.length x + List.length y + List.length aR + List.length bR))

The processor halts within lpB of the total input length.

theorem MIPRE.Tailored.Halting.classTV_efficient {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : (classTV TG U UT Λ₀ R).Efficient z

The class verifier is efficient on every input.

The outputs are those of the halting verifier

theorem MIPRE.Tailored.Halting.lenIs_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x : Cost.BitStr) (κ : Bool) (k : ℕ) : (classTV TG U UT Λ₀ R).LenIs z x κ k ↔ LenIs (VTz TG U UT Λ₀ R z).len (C TG) x κ k

The class calculator outputs what the compressed calculator outputs at the level C.

theorem MIPRE.Tailored.Halting.lpIs_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y aR bR : Cost.BitStr) (cs : List Cost.BitStr) : (classTV TG U UT Λ₀ R).LpIs z x y aR bR cs ↔ LpIs (VTz TG U UT Λ₀ R z).lp (C TG) x y aR bR cs

The class processor outputs what the processor of V^{R z, λ(z)} outputs at the level C.

theorem MIPRE.Tailored.Halting.lenOf_eq {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x : Cost.BitStr) (κ : Bool) : (classTV TG U UT Λ₀ R).lenOf z x κ = (VTz TG U UT Λ₀ R z).lenOf (C TG) x κ

theorem MIPRE.Tailored.Halting.lenDefined_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x : Cost.BitStr) : (classTV TG U UT Λ₀ R).LenDefined z x ↔ (VTz TG U UT Λ₀ R z).LenDefined (C TG) x

theorem MIPRE.Tailored.Halting.consOf_eq {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y aR bR : Cost.BitStr) : (classTV TG U UT Λ₀ R).consOf z x y aR bR = (VTz TG U UT Λ₀ R z).consOf (C TG) x y aR bR

The game

theorem MIPRE.Tailored.Halting.tgame_extends {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : ((classTV TG U UT Λ₀ R).tgame z).Extends ((VTz TG U UT Λ₀ R z).tgame (C TG)) (TG.samplerFamily.qEmb (C TG) Λ₀ R ⋯ z)

The class verifier's game extends that of V^{R z, λ(z)} at the level C, along the embedding of the questions as bit strings.

theorem MIPRE.Tailored.Halting.classTV_valStar {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : ((classTV TG U UT Λ₀ R).tgame z).valStar = (VTz TG U UT Λ₀ R z).valStar (C TG)

The value of the class verifier's game is that of V^{R z, λ(z)} at the level C.

theorem MIPRE.Tailored.Halting.classTV_hasPerfectZPC {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) (h : (VTz TG U UT Λ₀ R z).HasPerfectZPC (C TG)) : ((classTV TG U UT Λ₀ R).tgame z).doubled.HasPerfectZPC

A perfect ZPC strategy of V^{R z, λ(z)} at the level C is one of the class verifier's game, on the doubled games.

theorem MIPRE.Tailored.Halting.classTV_values {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : (Cost.Halts (R.toFun z) Cost.Data.nil → ((classTV TG U UT (lamThreshold TG U UT) R).tgame z).doubled.HasPerfectZPC) ∧ (¬Cost.Halts (R.toFun z) Cost.Data.nil → ((classTV TG U UT (lamThreshold TG U UT) R).tgame z).valStar ≤ 1 / 2)

The values on and off the language, at the threshold Λ₀ of lem:lambda.

RE ⊆ TMIP*, and TMIP* = RE

theorem MIPRE.Tailored.re_subset_tmipStar_of {ℓ : ℕ} (TG : TailoredGapCompression ℓ) {L : Set Cost.BitStr} (hL : IsRE L) : TMIPStar L

RE ⊆ TMIP* for the polynomial-time class, from a tailored gap compression.

theorem MIPRE.Tailored.tmipStar_eq_re_of {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : TMIPStar = IsRE

TMIP* = RE (II:787, thm:tailored_MIP*=RE), for the paper's polynomial-time class, from a tailored gap compression.