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

TMIPStar L → TMIPStarComputable L, hence TMIPStar ⊆ RE through TMIPStarComputable.isRE, as Foundations/ClassMIPStarTab.lean gives it for MIP*. On the input z, run the three programs of a polynomial-time tailored verifier under the budgets Efficient supplies and write the doubled game (V.tgame z).doubled down as a TailoredGameData (tabOfP):

• the vertices and the weights are those of PolyVerifier.tabOf: a tagged question (tg, x) at qIdx T tg x = idxOf x + N · tg, and one unit of weight per seed at the pair of tagged questions it produces;
• the lengths at a vertex are what the calculator outputs on its question (lenRunP), the question of the vertex v being the (v mod N)-th string (qOfIdx);
• the constraints at a pair of vertices and a readable part of the right length are what the processor outputs there (lpRunP).

presents_tabOfP: on an efficient input the tabulation presents the doubled game, so it has a perfect ZPC strategy when the doubled game does and the value of the game (MIPRE.Tailored.Presents).

The table

def MIPRE.Tailored.qOfIdx (T v : ℕ) : Cost.BitStr

The question at the vertex v: the (v mod N)-th string of length at most T, the vertex of the tagged question (tg, x) being qIdx T tg x = idxOf x + N · tg.

Equations

• MIPRE.Tailored.qOfIdx T v = (MIPRE.Cost.Data.bitStrsLE T).getD (v % MIPRE.PolyVerifier.N T) []

def MIPRE.Tailored.lenRunP (ld : Cost.Data) (P : Polynomial ℕ) (z x : Cost.BitStr) (κ : Bool) : ℕ

The length the calculator outputs on (z, x, κ) under the budget P(|z| + |x|), read in unary; 0 when the budget is missed.

Equations

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

def MIPRE.Tailored.lpRunP (pd : Cost.Data) (P : Polynomial ℕ) (z x y aR bR : Cost.BitStr) : List Cost.BitStr

The constraints the processor outputs on (z, x, y, a^R, b^R) under the budget P(|z| + |x| + |y| + |a^R| + |b^R|); [] when the budget is missed.

Equations

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

def MIPRE.Tailored.lenListP (ld : Cost.Data) (P : Polynomial ℕ) (z : Cost.BitStr) (κ : Bool) : List ℕ

The lengths at the vertices.

Equations

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

def MIPRE.Tailored.consAtP (pd : Cost.Data) (P : Polynomial ℕ) (z : Cost.BitStr) (lR : List ℕ) (v v' : ℕ) (γ : Cost.BitStr) : List (ℕ × ℕ × Cost.BitStr × Cost.BitStr)

The constraint entries at a pair of vertices and a readable part.

Equations

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

def MIPRE.Tailored.consTP (pd : Cost.Data) (P : Polynomial ℕ) (z : Cost.BitStr) (lR : List ℕ) : List (ℕ × ℕ × Cost.BitStr × Cost.BitStr)

The constraint entries.

Equations

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

def MIPRE.Tailored.tabOfP (sd ld pd : Cost.Data) (P : Polynomial ℕ) (z : Cost.BitStr) : TailoredGameValue.TailoredGameData

The table of the doubled game of a polynomial-time tailored verifier, from its three programs and its polynomial: the vertices and weights of PolyVerifier.tabOf, the lengths and constraints 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.Tailored.primrec_qOfIdx : Primrec₂ qOfIdx

theorem MIPRE.Tailored.primrec_lenRunP (ld : Cost.Data) (P : Polynomial ℕ) (κ : Bool) : Primrec fun (q : Cost.BitStr × Cost.BitStr) => lenRunP ld P q.1 q.2 κ

theorem MIPRE.Tailored.primrec_lpRunP (pd : Cost.Data) (P : Polynomial ℕ) {α : Type u_1} [Primcodable α] {z x y aR bR : α → Cost.BitStr} (hz : Primrec z) (hx : Primrec x) (hy : Primrec y) (haR : Primrec aR) (hbR : Primrec bR) : Primrec fun (a : α) => lpRunP pd P (z a) (x a) (y a) (aR a) (bR a)

theorem MIPRE.Tailored.primrec_T (P : Polynomial ℕ) : Primrec fun (z : Cost.BitStr) => Polynomial.eval (List.length z) P

theorem MIPRE.Tailored.primrec_lenListP (ld : Cost.Data) (P : Polynomial ℕ) (κ : Bool) : Primrec fun (z : Cost.BitStr) => lenListP ld P z κ

theorem MIPRE.Tailored.primrec_consAtP (pd : Cost.Data) (P : Polynomial ℕ) : Primrec fun (q : ((Cost.BitStr × List ℕ) × ℕ × ℕ) × Cost.BitStr) => consAtP pd P q.1.1.1 q.1.1.2 q.1.2.1 q.1.2.2 q.2

theorem MIPRE.Tailored.primrec_consTP_params (pd : Cost.Data) (P : Polynomial ℕ) : Primrec fun (q : Cost.BitStr × List ℕ) => consTP pd P q.1 q.2

theorem MIPRE.Tailored.primrec_tabOfP (sd ld pd : Cost.Data) (P : Polynomial ℕ) : Primrec (tabOfP sd ld pd P)

The table is primitive recursive in the input.

The vertices

theorem MIPRE.Tailored.qOfIdx_qEquiv (T : ℕ) (i : Fin (2 * PolyVerifier.N T)) : qOfIdx T ↑i = ↑((PolyVerifier.qEquiv T) i).2

The question of the vertex i of qEquiv is the string it names.

The runs, under the efficiency bounds

theorem MIPRE.Tailored.TPolyVerifier.lenIs_lenRunP (V : TPolyVerifier) {z x : Cost.BitStr} {κ : Bool} (hb : Cost.HaltsWithin V.len (Cost.encode (z, x, κ)) (Polynomial.eval (List.length z + List.length x) V.bound)) : V.LenIs z x κ (lenRunP (Cost.encode V.len) V.bound z x κ)

theorem MIPRE.Tailored.TPolyVerifier.lpIs_lpRunP (V : TPolyVerifier) {z x y aR bR : Cost.BitStr} (hb : Cost.HaltsWithin V.lp (Cost.encode (z, x, y, aR, bR)) (Polynomial.eval (List.length z + List.length x + List.length y + List.length aR + List.length bR) V.bound)) : V.LpIs z x y aR bR (lpRunP (Cost.encode V.lp) V.bound z x y aR bR)

theorem MIPRE.Tailored.TPolyVerifier.lenOf_eq_lenRunP (V : TPolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) (x : Cost.BitStr) (κ : Bool) : V.lenOf z x κ = lenRunP (Cost.encode V.len) V.bound z x κ

theorem MIPRE.Tailored.TPolyVerifier.consOf_eq_lpRunP (V : TPolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) (x y aR bR : Cost.BitStr) : V.consOf z x y aR bR = lpRunP (Cost.encode V.lp) V.bound z x y aR bR

The presentation

def MIPRE.Tailored.TPolyVerifier.tabP (V : TPolyVerifier) (z : Cost.BitStr) : TailoredGameValue.TailoredGameData

The table of V on z.

Equations

• V.tabP z = MIPRE.Tailored.tabOfP (MIPRE.Cost.encode V.sampler) (MIPRE.Cost.encode V.len) (MIPRE.Cost.encode V.lp) V.bound z

theorem MIPRE.Tailored.TPolyVerifier.computable_tabP (V : TPolyVerifier) : Computable V.tabP

theorem MIPRE.Tailored.TPolyVerifier.tabP_nV (V : TPolyVerifier) (z : Cost.BitStr) : (V.tabP z).nV + 1 = 2 * PolyVerifier.N (V.B z)

noncomputable def MIPRE.Tailored.TPolyVerifier.eP (V : TPolyVerifier) (z : Cost.BitStr) : Fin ((V.tabP z).nV + 1) ≃ Bool × Verifier.Answers (V.B z)

The vertices of the table, as the doubled questions: PolyVerifier.eX.

Equations

• V.eP z = V.toPoly.eX z

theorem MIPRE.Tailored.TPolyVerifier.qOfIdx_eP (V : TPolyVerifier) (z : Cost.BitStr) (i : Fin ((V.tabP z).nV + 1)) : qOfIdx (V.B z) ↑i = ↑((V.eP z) i).2

theorem MIPRE.Tailored.TPolyVerifier.lenList_getD_eP (V : TPolyVerifier) (z : Cost.BitStr) (κ : Bool) (i : Fin ((V.tabP z).nV + 1)) : (lenListP (Cost.encode V.len) V.bound z κ).getD (↑i) 0 = lenRunP (Cost.encode V.len) V.bound z (↑((V.eP z) i).2) κ

theorem MIPRE.Tailored.TPolyVerifier.mem_consTP (pd : Cost.Data) (P : Polynomial ℕ) (z : Cost.BitStr) (lR : List ℕ) (v v' : ℕ) (γ c : Cost.BitStr) : (v, v', γ, c) ∈ consTP pd P z lR ↔ v < 2 * PolyVerifier.N (Polynomial.eval (List.length z) P) ∧ v' < 2 * PolyVerifier.N (Polynomial.eval (List.length z) P) ∧ List.length γ = lR.getD v 0 + lR.getD v' 0 ∧ c ∈ lpRunP pd P z (qOfIdx (Polynomial.eval (List.length z) P) v) (qOfIdx (Polynomial.eval (List.length z) P) v') (List.take (lR.getD v 0) γ) (List.drop (lR.getD v 0) γ)

theorem MIPRE.Tailored.TPolyVerifier.presents_tabP (V : TPolyVerifier) {z : Cost.BitStr} (h : V.Efficient z) : Presents (V.tabP z) (V.tgame z).doubled (V.eP z)

The table presents the doubled game, on an efficient input.

theorem MIPRE.Tailored.TMIPStar.toComputable {L : Set Cost.BitStr} (h : TMIPStar L) : TMIPStarComputable L

TMIP* ⊆ TMIP*_computable: the table of the doubled game is a computable map with a perfect ZPC strategy on the members and the value of the game off them.

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

TMIP* ⊆ RE (II:1838), for the paper's class.