The paper's class is contained in the computable one: tabulation

Blueprint lem:mipstar-poly-sub: MIPStar L → MIPStarComputable L, hence MIPStar L → IsRE L through MIPStarComputable.isRE. A polynomial-time verifier is in particular a computable map from strings to explicit games: on the input z, run the sampler on every seed of length B z and the decider on every tuple of strings of length at most B z, each under the budget the efficiency clause supplies, and write the result down as a GameData.

Two things about the table, both inherited from Halting/Tabulate.lean:

• The questions are doubled. A GameData is read as a synchronous game, where unequal answers to equal questions lose by fiat, and G_z is a general bipartite game; tagging Alice's questions with false and Bob's with true puts no weight on the diagonal and quantumValue_doubled says the value is unchanged (Foundations/GameDouble.lean).
• Budgeted runs decide everything. Machine.runForD under the bound of PolyVerifier.Efficient returns the sampler's pair and the decider's verdict (Machine.runForD_eq_some_iff), so the table is primitive recursive in z and, on an efficient verifier, correct (quantumValue_tab).

The indexing: questions and answers are both indexed among the strings of length at most B z (Data.bitStrsLE), a tagged question (tg, x) at idxOf x + N · tg with N the number of such strings (qIdx, qEquiv), an answer at idxOf a (aEquiv).

Indexing the tagged strings of length at most T

@[reducible, inline]

abbrev MIPRE.PolyVerifier.N (T : ℕ) : ℕ

The number of strings of length at most T.

Equations

• MIPRE.PolyVerifier.N T = (MIPRE.Cost.Data.bitStrsLE T).length

theorem MIPRE.PolyVerifier.length_answerList_eq (T : ℕ) : (Verifier.answerList T).length = N T

def MIPRE.PolyVerifier.qIdx (T : ℕ) (tg : Bool) (x : Cost.BitStr) : ℕ

The index of the tagged question (tg, x).

Equations

• MIPRE.PolyVerifier.qIdx T tg x = List.idxOf x (MIPRE.Cost.Data.bitStrsLE T) + MIPRE.PolyVerifier.N T * if tg = true then 1 else 0

noncomputable def MIPRE.PolyVerifier.qEquiv (T : ℕ) : Fin (2 * N T) ≃ Bool × Verifier.Answers T

The tagged question alphabet, indexed.

Equations

• MIPRE.PolyVerifier.qEquiv T = finProdFinEquiv.symm.trans (finTwoEquiv.prodCongr ((finCongr ⋯).trans (MIPRE.Verifier.answerEquiv T)))

noncomputable def MIPRE.PolyVerifier.aEquiv (T : ℕ) : Fin (N T) ≃ Verifier.Answers T

The answer alphabet, indexed among the strings of length at most T.

Equations

• MIPRE.PolyVerifier.aEquiv T = (finCongr ⋯).trans (MIPRE.Verifier.answerEquiv T)

theorem MIPRE.PolyVerifier.aEquiv_apply (T : ℕ) (k : Fin (N T)) : List.idxOf (↑((aEquiv T) k)) (Cost.Data.bitStrsLE T) = ↑k

theorem MIPRE.PolyVerifier.finTwoEquiv_ite (a : Fin 2) : (if finTwoEquiv a = true then 1 else 0) = ↑a

theorem MIPRE.PolyVerifier.qEquiv_apply (T : ℕ) (i : Fin (2 * N T)) : qIdx T ((qEquiv T) i).1 ↑((qEquiv T) i).2 = ↑i

theorem MIPRE.PolyVerifier.qIdx_lt (T : ℕ) (tg : Bool) {x : Cost.BitStr} (hx : x ∈ Cost.Data.bitStrsLE T) : qIdx T tg x < 2 * N T

theorem MIPRE.PolyVerifier.qIdx_inj (T : ℕ) {tg tg' : Bool} {x x' : Cost.BitStr} (hx : x ∈ Cost.Data.bitStrsLE T) (hx' : x' ∈ Cost.Data.bitStrsLE T) (h : qIdx T tg x = qIdx T tg' x') : tg = tg' ∧ x = x'

The table

def MIPRE.PolyVerifier.sampleC (sd : Cost.Data) (T : ℕ) (z r : Cost.BitStr) : Cost.BitStr × Cost.BitStr

The sampler's pair on (z, r) under the budget T, read off a budgeted run; ([], []) if the run does not finish or its result is not a pair of strings.

Equations

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

def MIPRE.PolyVerifier.accC (pd : Cost.Data) (P : Polynomial ℕ) (z x y a b : Cost.BitStr) : Bool

The decider's verdict on (z, x, y, a, b) under the budget P(|z| + |x| + |y| + |a| + |b|).

Equations

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

def MIPRE.PolyVerifier.accListLE (T : ℕ) (fA fB : Cost.BitStr → ℕ) (acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool) : List (ℕ × ℕ × ℕ × ℕ)

The acceptance table over four copies of the strings of length at most T.

Equations

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

theorem MIPRE.PolyVerifier.mem_accListLE_iff {T : ℕ} {fA fB : Cost.BitStr → ℕ} {acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool} {i j k l : ℕ} : (i, j, k, l) ∈ accListLE T fA fB acc? ↔ ∃ x ∈ Cost.Data.bitStrsLE T, ∃ y ∈ Cost.Data.bitStrsLE T, ∃ a ∈ Cost.Data.bitStrsLE T, ∃ b ∈ Cost.Data.bitStrsLE T, acc? x y a b = true ∧ i = fA x ∧ j = fB y ∧ k = List.idxOf a (Cost.Data.bitStrsLE T) ∧ l = List.idxOf b (Cost.Data.bitStrsLE T)

def MIPRE.PolyVerifier.tuplesLE (T : ℕ) : List (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr)

The four-fold product of the enumeration, as one flat list.

Equations

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

theorem MIPRE.PolyVerifier.primrec_tuplesLE : Primrec tuplesLE

theorem MIPRE.PolyVerifier.accListLE_eq_filterMap (T : ℕ) (fA fB : Cost.BitStr → ℕ) (acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool) : accListLE T fA fB acc? = List.filterMap (fun (q : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => if acc? q.1 q.2.1 q.2.2.1 q.2.2.2 = true then some (fA q.1, fB q.2.1, List.idxOf q.2.2.1 (Cost.Data.bitStrsLE T), List.idxOf q.2.2.2 (Cost.Data.bitStrsLE T)) else none) (tuplesLE T)

theorem MIPRE.PolyVerifier.primrec_accListLE {α : Type u_1} [Primcodable α] {T : α → ℕ} {fA fB : α → Cost.BitStr → ℕ} {acc? : α → Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool} (hT : Primrec T) (hfA : Primrec₂ fA) (hfB : Primrec₂ fB) (hacc : Primrec fun (q : α × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => acc? q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2) : Primrec fun (a : α) => accListLE (T a) (fA a) (fB a) (acc? a)

def MIPRE.PolyVerifier.tabOf (sd pd : Cost.Data) (P : Polynomial ℕ) (z : Cost.BitStr) : HaltingGameValue.GameData

The table of G_z, from the two programs and the polynomial: doubled questions indexed by qIdx, one unit of weight per seed, and the acceptance table by budgeted runs.

Equations

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

The table is primitive recursive in the input

theorem MIPRE.PolyVerifier.primrec_qIdx (tg : Bool) : Primrec₂ fun (T : ℕ) (x : Cost.BitStr) => qIdx T tg x

theorem MIPRE.PolyVerifier.primrec_sampleC (sd : Cost.Data) : Primrec fun (q : (ℕ × Cost.BitStr) × Cost.BitStr) => sampleC sd q.1.1 q.1.2 q.2

theorem MIPRE.PolyVerifier.primrec_accC (pd : Cost.Data) (P : Polynomial ℕ) : Primrec fun (q : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => accC pd P q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2

theorem MIPRE.PolyVerifier.primrec_tabOf (sd pd : Cost.Data) (P : Polynomial ℕ) : Primrec (tabOf sd pd P)

The table of a verifier, and its correctness on an efficient input

def MIPRE.PolyVerifier.tab (V : PolyVerifier) (z : Cost.BitStr) : HaltingGameValue.GameData

The table of G_z.

Equations

• V.tab z = MIPRE.PolyVerifier.tabOf (MIPRE.Cost.encode V.sampler) (MIPRE.Cost.encode V.decider) V.bound z

theorem MIPRE.PolyVerifier.tab_computable (V : PolyVerifier) : Computable V.tab

theorem MIPRE.PolyVerifier.tab_nX (V : PolyVerifier) (z : Cost.BitStr) : (V.tab z).nX + 1 = 2 * N (V.B z)

theorem MIPRE.PolyVerifier.tab_nA (V : PolyVerifier) (z : Cost.BitStr) : (V.tab z).nA + 1 = N (V.B z)

noncomputable def MIPRE.PolyVerifier.eX (V : PolyVerifier) (z : Cost.BitStr) : Fin ((V.tab z).nX + 1) ≃ Bool × Verifier.Answers (V.B z)

The question relabeling.

Equations

• V.eX z = (finCongr ⋯).trans (MIPRE.PolyVerifier.qEquiv (V.B z))

noncomputable def MIPRE.PolyVerifier.eA (V : PolyVerifier) (z : Cost.BitStr) : Fin ((V.tab z).nA + 1) ≃ Verifier.Answers (V.B z)

The answer relabeling.

Equations

• V.eA z = (finCongr ⋯).trans (MIPRE.PolyVerifier.aEquiv (V.B z))

theorem MIPRE.PolyVerifier.eX_apply (V : PolyVerifier) (z : Cost.BitStr) (i : Fin ((V.tab z).nX + 1)) : qIdx (V.B z) ((V.eX z) i).1 ↑((V.eX z) i).2 = ↑i

theorem MIPRE.PolyVerifier.eA_apply (V : PolyVerifier) (z : Cost.BitStr) (k : Fin ((V.tab z).nA + 1)) : List.idxOf (↑((V.eA z) k)) (Cost.Data.bitStrsLE (V.B z)) = ↑k

theorem MIPRE.PolyVerifier.qIdx_eq_iff' (V : PolyVerifier) (z : Cost.BitStr) (tg : Bool) {x : Cost.BitStr} (hx : x ∈ Cost.Data.bitStrsLE (V.B z)) (i : Fin ((V.tab z).nX + 1)) : qIdx (V.B z) tg x = ↑i ↔ tg = ((V.eX z) i).1 ∧ x = ↑((V.eX z) i).2

theorem MIPRE.PolyVerifier.sampleC_eq (V : PolyVerifier) {z : Cost.BitStr} (h : V.SamplerRuns z) {r : Cost.BitStr} (hr : List.length r = V.B z) : sampleC (Cost.encode V.sampler) (Polynomial.eval (List.length z + V.B z) V.bound) z r = (↑(V.questions z r).1, ↑(V.questions z r).2)

The budgeted sample is the question pair, on an efficient input and a seed of the right length.

theorem MIPRE.PolyVerifier.accC_eq (V : PolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) (x y a b : Cost.BitStr) : accC (Cost.encode V.decider) V.bound z x y a b = true ↔ V.Accepts z x y a b

The budgeted verdict is acceptance, on an efficient input.

theorem MIPRE.PolyVerifier.sampleC_fst_mem (V : PolyVerifier) {z : Cost.BitStr} (h : V.SamplerRuns z) {r : Cost.BitStr} (hr : r ∈ Cost.Data.bitStrsOfLen (V.B z)) : (sampleC (Cost.encode V.sampler) (Polynomial.eval (List.length z + V.B z) V.bound) z r).1 ∈ Cost.Data.bitStrsLE (V.B z)

theorem MIPRE.PolyVerifier.sampleC_snd_mem (V : PolyVerifier) {z : Cost.BitStr} (h : V.SamplerRuns z) {r : Cost.BitStr} (hr : r ∈ Cost.Data.bitStrsOfLen (V.B z)) : (sampleC (Cost.encode V.sampler) (Polynomial.eval (List.length z + V.B z) V.bound) z r).2 ∈ Cost.Data.bitStrsLE (V.B z)

theorem MIPRE.PolyVerifier.mu_clause (V : PolyVerifier) {z : Cost.BitStr} (h : V.SamplerRuns z) (i j : Fin ((V.tab z).nX + 1)) : (V.tab z).game.μ i j = (V.game z).doubled.μ ((V.eX z) i) ((V.eX z) j)

The μ clause, doubled: the tabulated distribution is μ_z on the block (false, ·) × (true, ·) and zero elsewhere.

theorem MIPRE.PolyVerifier.acc_mem_iff (V : PolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) (i j : Fin ((V.tab z).nX + 1)) (k l : Fin ((V.tab z).nA + 1)) : (↑i, ↑j, ↑k, ↑l) ∈ (V.tab z).acc ↔ ((V.eX z) i).1 = false ∧ ((V.eX z) j).1 = true ∧ V.Accepts z ↑((V.eX z) i).2 ↑((V.eX z) j).2 ↑((V.eA z) k) ↑((V.eA z) l)

The acceptance table read back, doubled.

theorem MIPRE.PolyVerifier.D_clause (V : PolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) (i j : Fin ((V.tab z).nX + 1)) (k l : Fin ((V.tab z).nA + 1)) : (V.tab z).game.D i j k l = (V.game z).doubled.D ((V.eX z) i) ((V.eX z) j) ((V.eA z) k) ((V.eA z) l)

The D clause, doubled.

theorem MIPRE.PolyVerifier.quantumValue_tab (V : PolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) : quantumValue (V.tab z).game = quantumValue (V.game z)

The table has the value of G_z, on an efficient input.

theorem MIPRE.MIPStar.toComputable {L : Set Cost.BitStr} (h : MIPStar L) : MIPStarComputable L

lem:mipstar-poly-sub: the paper's class is contained in the computable one.

theorem MIPRE.MIPStar.isRE {L : Set Cost.BitStr} (h : MIPStar L) : IsRE L

The paper's class is contained in RE.