The classes RE, coRE and MIPClass ω, and the inclusions MIP* ⊆ RE, MIP^co ⊆ coRE

Blueprint def:re, def:core, def:mipstar-computable, def:mipco, and the easy halves of thm:mipstar-eq-re and thm:mipco-eq-core, written once in a value model ω (ValueModel):

• IsRE L: the language L ⊆ {0,1}* is recursively enumerable — membership is an REPred, the domain of a partial computable function; equivalently (isRE_iff) the halting set of a well-scoped program of the ambient model on encoded strings. IsCoRE L: its complement is.
• MIPClass ω L: there is a computable map from strings to game descriptions (GameData, def:game-description) with value 1 in the model for x ∈ L and at most 1/2 for x ∉ L. MIPStarComputable is MIPClass ValueModel.tensor and MIPCo is MIPClass ValueModel.commuting. These are the computable versions of the classes, with games given as explicit descriptions. The paper's definition asks for a polynomial-time verifier (a sampler and a decider running in time polynomial in |x|); the class it defines is contained in this one, since a polynomial-time verifier is in particular a computable map to the finite game it describes (MIPStar.toComputable, ClassMIPStarTab.lean). The computable version is the one the Lean main statement uses (HaltingGameValue.halting_reduces_to_gameValue), and the inclusion in RE proved here for the larger class implies it for the smaller.
• MIPClass.isRE: MIPClass ω ⊆ RE when the value is r.e. from below (ValueModel.LowerRE), at the threshold 1/2: under the promise, x ∈ L ↔ val(G_x) > 1/2. At tensor (ValueModel.tensor_lowerRE, from lem:value-lower-approx) this is MIP* ⊆ RE.
• MIPClass.isCoRE: MIPClass ω ⊆ coRE when the value is r.e. from above (ValueModel.UpperRE), at the threshold 1: under the promise, x ∉ L ↔ val(G_x) < 1. At commuting (ValueModel.commuting_upperRE, Tsirelson/UpperRE.lean) this is MIP^co ⊆ coRE, the role Lin's proof gives to the NPA hierarchy (Lin25).
• exists_semidecider_lt_quantumValue: the Prog form — for a computable family of game descriptions, a well-scoped program of the ambient model halting exactly on the x with p/q < val*(G_x); the hypothesis hS of Cost.compressibility_criterion for B the strings whose game has value at most p/q.

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

def:re. A language is recursively enumerable if membership is the domain of a partial computable function (Mathlib's REPred).

Equations

• MIPRE.IsRE L = REPred fun (x : MIPRE.Cost.BitStr) => x ∈ L

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

def:core. A language is co-recursively enumerable if its complement is.

Equations

• MIPRE.IsCoRE L = MIPRE.IsRE Lᶜ

theorem MIPRE.isCoRE_iff (L : Set Cost.BitStr) : IsCoRE L ↔ REPred fun (x : Cost.BitStr) => x ∉ L

def MIPRE.MIPClass (ω : ValueModel) (L : Set Cost.BitStr) : Prop

The class of a value model, computable version (def:mipstar-computable at ValueModel.tensor, def:mipco at ValueModel.commuting). A language L is in MIPClass ω if there is a computable map from strings to game descriptions such that the game of x has value 1 in the model when x ∈ L and at most 1/2 when x ∉ L.

Equations

• MIPRE.MIPClass ω L = ∃ (g : MIPRE.Cost.BitStr → HaltingGameValue.GameData), Computable g ∧ ∀ (x : MIPRE.Cost.BitStr), (x ∈ L → ω.val (g x).game = 1) ∧ (x ∉ L → ω.val (g x).game ≤ 1 / 2)

@[reducible, inline]

abbrev MIPRE.MIPStarComputable : Set Cost.BitStr → Prop

def:mipstar, computable version: MIPClass at the tensor-product value.

Equations

• MIPRE.MIPStarComputable = MIPRE.MIPClass MIPRE.ValueModel.tensor

@[reducible, inline]

abbrev MIPRE.MIPCo : Set Cost.BitStr → Prop

def:mipco, computable version: MIPClass at the commuting-operator value.

Equations

• MIPRE.MIPCo = MIPRE.MIPClass MIPRE.ValueModel.commuting

theorem MIPRE.REPred.comp' {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : β → Prop} (hp : REPred p) {g : α → β} (hg : Computable g) : REPred fun (a : α) => p (g a)

Precomposition of an r.e. predicate with a computable function.

theorem MIPRE.rePred_lt_quantumValue_comp {α : Type u_1} [Primcodable α] {g : α → HaltingGameValue.GameData} (hg : Computable g) (p q : ℕ) : REPred fun (x : α) => ↑p / ↑q < quantumValue (g x).game

lem:value-lower-approx along a computable family of game descriptions: the x with p / q < val*(G_{g x}) form an r.e. set.

theorem MIPRE.ValueModel.tensor_lowerRE : tensor.LowerRE

The tensor-product value is r.e. from below (blueprint lem:value-lower-approx).

theorem MIPRE.ValueModel.LowerRE.comp {ω : ValueModel} (hlow : ω.LowerRE) {α : Type u_1} [Primcodable α] {g : α → HaltingGameValue.GameData} (hg : Computable g) (p q : ℕ) : REPred fun (x : α) => ↑p / ↑q < ω.val (g x).game

A lower semidecider for the value along a computable family of game descriptions: the x with p / q < val(G_{g x}) form an r.e. set.

theorem MIPRE.ValueModel.UpperRE.comp {ω : ValueModel} (hup : ω.UpperRE) {α : Type u_1} [Primcodable α] {g : α → HaltingGameValue.GameData} (hg : Computable g) (p q : ℕ) : REPred fun (x : α) => ω.val (g x).game < ↑p / ↑q

An upper semidecider for the value along a computable family of game descriptions: the x with val(G_{g x}) < p / q form an r.e. set.

theorem MIPRE.MIPClass.isRE {ω : ValueModel} (hlow : ω.LowerRE) {L : Set Cost.BitStr} (h : MIPClass ω L) : IsRE L

MIPClass ω ⊆ RE when the value is r.e. from below (the easy half of thm:mipstar-eq-re): enumerate the witnesses of val(G_x) > 1/2.

theorem MIPRE.MIPClass.isCoRE {ω : ValueModel} (hup : ω.UpperRE) {L : Set Cost.BitStr} (h : MIPClass ω L) : IsCoRE L

MIPClass ω ⊆ coRE when the value is r.e. from above (the easy half of thm:mipco-eq-core): the complement of L is the preimage of the r.e. set of descriptions with val < 1 under the computable map.

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

MIP* ⊆ RE (the easy half of thm:mipstar-eq-re): enumerate strategies of the game of x and accept upon finding one of value greater than 1/2.

theorem MIPRE.isRE_iff (L : Set Cost.BitStr) : IsRE L ↔ ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ x ∈ L

Recursive enumerability in the ambient model: a language is r.e. iff it is the halting set of a well-scoped program on encoded strings.

theorem MIPRE.MIPClass.exists_semidecider {ω : ValueModel} (hlow : ω.LowerRE) {L : Set Cost.BitStr} (h : MIPClass ω L) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ x ∈ L

A language in MIPClass ω, for a value r.e. from below, is the halting set of a program of the ambient model.

theorem MIPRE.MIPClass.exists_cosemidecider {ω : ValueModel} (hup : ω.UpperRE) {L : Set Cost.BitStr} (h : MIPClass ω L) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ x ∉ L

The complement of a language in MIPClass ω, for a value r.e. from above, is the halting set of a program of the ambient model.

theorem MIPRE.MIPStarComputable.exists_semidecider {L : Set Cost.BitStr} (h : MIPStarComputable L) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ x ∈ L

A language in MIP* is the halting set of a program of the ambient model.

theorem MIPRE.exists_semidecider_lt_quantumValue {g : Cost.BitStr → HaltingGameValue.GameData} (hg : Computable g) (p q : ℕ) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ ↑p / ↑q < quantumValue (g x).game

The semidecider of the compressibility criterion. For a computable family of game descriptions and a threshold p / q, a well-scoped program halting on encode x exactly when p / q < val*(G_{g x}): the hypothesis hS of Cost.compressibility_criterion, with B the strings whose game has value at most p / q.