The class MIP*_{1,1/2}(2,1) as the paper defines it

Blueprint def:mipstar, the paper's form (games.tex, Definition "def:mipstar"): a language L is in the class if there are two machines, a sampler 𝒮 and a decider 𝒟, such that for every string z there is a finite game G_z with

• efficiency: 𝒮 on input z runs in time poly(|z|) and returns a question pair distributed as μ_z; 𝒟 on input (z, x, y, a, b) runs in time poly(|z|) and returns D_z(x, y, a, b), returning 0 whenever x, y, a, b are too long (the paper's footnote);
• completeness: z ∈ L → val*(G_z) = 1;
• soundness: z ∉ L → val*(G_z) ≤ 1/2.

MIPRE.MIPStarComputable (ClassMIPStarComputable.lean) is the computable version of this, with G_z an explicit GameData computed from z with no time bound; planning/polytime-halting.md has why the two are different and what it takes to prove RE ⊆ the class below. This file is the class itself.

The reading

A PolyVerifier is a closed sampler program, a closed decider program and one polynomial P; write B z = P.eval |z|.

• A randomized machine is a deterministic program with an explicit uniform seed of the length of its time bound: the sampler runs on encode (z, r) for a seed r of length B z. The question distribution μ_z is the pushforward of the uniform seed.
• The decider's time is polynomial in the total input length |z| + |x| + |y| + |a| + |b|, not in |z| alone: a program of the ambient model reads a list only by walking it (blueprint, the discussion under def:decider), so the paper's "poly(|z|) even for long inputs" is not expressible here. The paper's own device, the footnote's rejection of overlong messages, is a separate clause (Efficient.rejects_long), and the game G_z lives on the strings of length at most B z, which makes it the paper's finite game.
• The output of the sampler is read as a pair of strings of length at most B z; on an efficient verifier it always is one (Efficient.sampler_runs), and the fallback ([], []) of PolyVerifier.questions is never taken. It is there so that game is total.

MIPStar.toComputable (ClassMIPStarTab.lean) is the inclusion in the computable class, by tabulation, which gives MIPStar ⊆ RE from MIPStarComputable.isRE.

structure MIPRE.PolyVerifier : Type

A polynomial-time verifier (def:mipstar, the paper's form): a sampler, a decider and one polynomial time bound.

• sampler : Cost.Prog

  The sampler program; its input is encode (z, r) for the input z and a seed r.

• sampler_closed : Cost.Prog.WellScoped 1 self.sampler

  It is closed.

• decider : Cost.Prog

  The decider program; its input is encode (z, x, y, a, b).

• decider_closed : Cost.Prog.WellScoped 1 self.decider

  It is closed.

• bound : Polynomial ℕ

  The polynomial P of the time bounds.

def MIPRE.PolyVerifier.B (V : PolyVerifier) (z : Cost.BitStr) : ℕ

The bound B z = P(|z|): the seed length, the sampler's time on z, and the length of the questions and answers of G_z.

Equations

• V.B z = Polynomial.eval (List.length z) V.bound

def MIPRE.PolyVerifier.Accepts (V : PolyVerifier) (z x y a b : Cost.BitStr) : Prop

The decider accepts (z, x, y, a, b): it halts with output 1.

Equations

• V.Accepts z x y a b = ∃ (t : ℕ), V.decider.Runs (MIPRE.Cost.encode (z, x, y, a, b)) (MIPRE.Cost.encode true) t

noncomputable def MIPRE.PolyVerifier.sample? (V : PolyVerifier) (z r : Cost.BitStr) : Option (Cost.BitStr × Cost.BitStr)

The sampler's output on (z, r), if it halts with (the encoding of) a pair of strings.

Equations

• V.sample? z r = if h : ∃ (p : MIPRE.Cost.BitStr × MIPRE.Cost.BitStr) (t : ℕ), V.sampler.Runs (MIPRE.Cost.encode (z, r)) (MIPRE.Cost.encode p) t then some h.choose else none

theorem MIPRE.PolyVerifier.sample?_eq_some_iff (V : PolyVerifier) (z r : Cost.BitStr) (p : Cost.BitStr × Cost.BitStr) : V.sample? z r = some p ↔ ∃ (t : ℕ), V.sampler.Runs (Cost.encode (z, r)) (Cost.encode p) t

def MIPRE.PolyVerifier.emptyAnswer (T : ℕ) : Verifier.Answers T

The empty answer, in the alphabet of length at most T.

Equations

• MIPRE.PolyVerifier.emptyAnswer T = ⟨[], ⋯⟩

noncomputable def MIPRE.PolyVerifier.questions (V : PolyVerifier) (z r : Cost.BitStr) : Verifier.Answers (V.B z) × Verifier.Answers (V.B z)

The question pair a seed produces: the sampler's output, when it is a pair of strings of length at most B z, and ([], []) otherwise.

Equations

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

def MIPRE.PolyVerifier.SamplerRuns (V : PolyVerifier) (z : Cost.BitStr) : Prop

The sampler, on every seed of length B z, halts within cost P(|z| + |r|) with a pair of strings of length at most B z. The bound is in the total input length, as the decider's: a program reads its seed only by walking it, so B z itself would leave no time to read a seed of length B z; with |r| = B z polynomial in |z| the bound is still poly(|z|). This is the sampler's clause of Efficient, which is all the question distribution needs.

Equations

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

structure MIPRE.PolyVerifier.Efficient (V : PolyVerifier) (z : Cost.BitStr) : Prop

Efficiency on the input z (def:mipstar, item 1).

• sampler_runs : V.SamplerRuns z

  The sampler's clause (SamplerRuns).

• decider_time (x y a b : Cost.BitStr) : Cost.HaltsWithin V.decider (Cost.encode (z, x, y, a, b)) (Polynomial.eval (List.length z + List.length x + List.length y + List.length a + List.length b) V.bound)

  The decider halts within cost P(|z| + |x| + |y| + |a| + |b|) on every input.

• rejects_long (x y a b : Cost.BitStr) : V.B z < List.length x ∨ V.B z < List.length y ∨ V.B z < List.length a ∨ V.B z < List.length b → ¬V.Accepts z x y a b

  The decider rejects whenever one of the four strings is longer than B z.

theorem MIPRE.PolyVerifier.questions_eq_of_samplerRuns (V : PolyVerifier) {z : Cost.BitStr} (h : V.SamplerRuns z) {r : Cost.BitStr} (hr : List.length r = V.B z) : ∃ (x : Cost.BitStr) (y : Cost.BitStr), ∃ t ≤ Polynomial.eval (List.length z + List.length r) V.bound, V.sampler.Runs (Cost.encode (z, r)) (Cost.encode (x, y)) t ∧ ↑(V.questions z r).1 = x ∧ ↑(V.questions z r).2 = y

Under the sampler's clause the sampler's output on a seed of the right length is the question pair, with no fallback.

theorem MIPRE.PolyVerifier.questions_eq_of_efficient (V : PolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) {r : Cost.BitStr} (hr : List.length r = V.B z) : ∃ (x : Cost.BitStr) (y : Cost.BitStr), ∃ t ≤ Polynomial.eval (List.length z + List.length r) V.bound, V.sampler.Runs (Cost.encode (z, r)) (Cost.encode (x, y)) t ∧ ↑(V.questions z r).1 = x ∧ ↑(V.questions z r).2 = y

On an efficient verifier the sampler's output on a seed of the right length is the question pair, with no fallback.

The game G_z

noncomputable def MIPRE.PolyVerifier.seedCount (V : PolyVerifier) (z : Cost.BitStr) (x y : Verifier.Answers (V.B z)) : ℕ

The number of seeds of length B z producing the question pair (x, y).

Equations

• V.seedCount z x y = (List.filter (fun (r : MIPRE.Cost.BitStr) => decide (V.questions z r = (x, y))) (MIPRE.Cost.Data.bitStrsOfLen (V.B z))).length

theorem MIPRE.PolyVerifier.sum_length_filter_eq {A : Type u_1} [Fintype A] [DecidableEq A] (f : Cost.BitStr → A × A) (l : List Cost.BitStr) : ∑ x : A, ∑ y : A, (List.filter (fun (r : Cost.BitStr) => decide (f r = (x, y))) l).length = l.length

Summing a list's fibres over a finite codomain counts the list.

noncomputable def MIPRE.PolyVerifier.game (V : PolyVerifier) (z : Cost.BitStr) : Game (Verifier.Answers (V.B z)) (Verifier.Answers (V.B z)) (Verifier.Answers (V.B z)) (Verifier.Answers (V.B z))

The game G_z of the verifier on the input z: questions and answers are the strings of length at most B z, the question pair is the sampler's output on a uniform seed, and the decision is the decider's.

Equations

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

theorem MIPRE.PolyVerifier.game_μ (V : PolyVerifier) (z : Cost.BitStr) (x y : Verifier.Answers (V.B z)) : (V.game z).μ x y = ↑(V.seedCount z x y) / 2 ^ V.B z

theorem MIPRE.PolyVerifier.game_D (V : PolyVerifier) (z : Cost.BitStr) (x y a b : Verifier.Answers (V.B z)) : (V.game z).D x y a b = decide (V.Accepts z ↑x ↑y ↑a ↑b)

def MIPRE.MIPStar (L : Set Cost.BitStr) : Prop

def:mipstar, the paper's class MIP*_{1,1/2}(2,1). A language L is in it if some polynomial-time verifier is efficient on every input, and its game has quantum value 1 on the members of L and at most 1/2 off them.

Equations

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