The commuting-operator value is recursively enumerable from above

Step §3.6 of the Tsirelson route (planning/tsirelson-campaign.md): the coded certificate check MIPRE.Tsirelson.Coded.CheckUpper of MIPRE.Foundations.Tsirelson.CodedPoly decides exactly the certificates of MIPRE.Foundations.Tsirelson.Certificate, so the thresholds above the commuting-operator value of a described game form a recursively enumerable set (commutingUpperRE, blueprint lem:valco-upper-re), and with the halting reduction the negative answer to Tsirelson's problem follows (tsirelson_of_haltingReduction).

Decoding. For a game description d with nX, nA, both players of d.game have questions Fin (nX + 1) and answers Fin (nA + 1), and the letters of its game algebra are FinGen nX nA. A coded letter inl (x, a) decodes to e_xa and inr (y, b) to f_yb, with the indices clamped into range (decodeLetter), a coded word to the product of its letters (decodeWord), and a coded polynomial [(w, c), …] to Σ c · w (interp). The decoding is a homomorphism for every coded operation, with no validity hypothesis: sums (interp_append), negation, scaling, products (interp_cmul) and the star (interp_cstar). Every relation index decodes to one of the relations rels (interp_relPoly_mem), and every relation is the decoding of a valid index (exists_relIdx). The coded game polynomial is W_d times the game polynomial (interp_Wint), since μ(x, y) = wt(x, y) / W_d and the predicates agree.

Coefficients. On valid letters, encodeLetter is a left inverse of the decoding, so decodeWord is injective on valid words (decodeWord_injOn). Hence the merged coefficient of a valid word in a valid coded polynomial is the coefficient of its decoding (coeff_interp), the support of the decoding lies in the decoded words (support_interp_subset), and the coded dominance test is the dominance of the decoding (isDominant_iff_dominant_interp).

The check. A certificate decodes to a scale N, hermitian squares and ideal monomials (decodeSos, decodeIdeal), and its residual to

N² (κ r·1 - κ W_G) - Σ s⋆ g s - Σ c · w ρ w', κ = q·W_d, r = p / q

(interp_certR_eq), the residual of Certificate. So an accepted certificate bounds the value below p / q (checkUpper_sound, by commutingOperatorValue_lt_of_certificate). Conversely, if the value is below p / q, then q > 0 (for q = 0 the threshold is 0, and the value is nonnegative), and exists_certificate_of_lt gives a certificate with Gaussian-integer coefficients, which is encoded exactly (encodeC, encodePoly, encodeSos, encodeIdeal) into an accepted coded certificate (checkUpper_complete).

Main declarations

• FinGen, FinRels, decodeLetter, encodeLetter, decodeWord, encodeWord, decodeWord_injOn;
• interp, interp_append, interp_cneg, interp_cscale, interp_cmul, interp_cstar, interp_relPoly_mem, exists_relIdx, interp_Wint;
• coeff_interp, support_interp_subset, isDominant_iff_dominant_interp;
• decodeSos, decodeIdeal, interp_certR_eq, checkUpper_sound;
• encodeC, encodePoly, encodeSos, encodeIdeal, checkUpper_complete, checkUpper_iff;
• MIPRE.commutingUpperRE, MIPRE.tsirelson_of_haltingReduction.

Letters and words

@[reducible, inline]

abbrev MIPRE.Tsirelson.FinGen (nX nA : ℕ) : Type

The letters of the game algebra of a described game: both players have questions Fin (nX + 1) and answers Fin (nA + 1).

Equations

• MIPRE.Tsirelson.FinGen nX nA = MIPRE.Tsirelson.Gen (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))

@[reducible, inline]

abbrev MIPRE.Tsirelson.FinRels (nX nA : ℕ) : Set (NCPoly (FinGen nX nA))

The relations of the game algebra of a described game.

Equations

• MIPRE.Tsirelson.FinRels nX nA = MIPRE.Tsirelson.rels (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))

def MIPRE.Tsirelson.finOf (n a : ℕ) : Fin (n + 1)

A natural clamped into Fin (n + 1).

Equations

• MIPRE.Tsirelson.finOf n a = ⟨min a n, ⋯⟩

theorem MIPRE.Tsirelson.val_finOf {n a : ℕ} (h : a ≤ n) : ↑(finOf n a) = a

The clamp is the identity in range.

@[simp]

theorem MIPRE.Tsirelson.finOf_val {n : ℕ} (i : Fin (n + 1)) : finOf n ↑i = i

Clamping the value of an element of Fin (n + 1) returns it.

def MIPRE.Tsirelson.decodeLetter (nX nA : ℕ) : Coded.Letter → FinGen nX nA

The decoding of a coded letter: inl (x, a) is e_xa and inr (y, b) is f_yb, with the indices clamped into range.

Equations

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

def MIPRE.Tsirelson.encodeLetter {nX nA : ℕ} : FinGen nX nA → Coded.Letter

The code of a letter.

Equations

• MIPRE.Tsirelson.encodeLetter = Sum.map (fun (p : Fin (nX + 1) × Fin (nA + 1)) => (↑p.1, ↑p.2)) fun (p : Fin (nX + 1) × Fin (nA + 1)) => (↑p.1, ↑p.2)

@[simp]

theorem MIPRE.Tsirelson.decodeLetter_encodeLetter {nX nA : ℕ} (g : FinGen nX nA) : decodeLetter nX nA (encodeLetter g) = g

Decoding inverts the code of a letter.

theorem MIPRE.Tsirelson.encodeLetter_decodeLetter {nX nA : ℕ} {l : Coded.Letter} (h : Coded.ValidLetter nX nA l) : encodeLetter (decodeLetter nX nA l) = l

On valid letters, the code inverts the decoding.

theorem MIPRE.Tsirelson.validLetter_encodeLetter {nX nA : ℕ} (g : FinGen nX nA) : Coded.ValidLetter nX nA (encodeLetter g)

The code of a letter is valid.

def MIPRE.Tsirelson.decodeWord (nX nA : ℕ) (w : List Coded.Letter) : FreeMonoid (FinGen nX nA)

The decoding of a coded word: the product of its decoded letters.

Equations

• MIPRE.Tsirelson.decodeWord nX nA w = FreeMonoid.ofList (List.map (MIPRE.Tsirelson.decodeLetter nX nA) w)

def MIPRE.Tsirelson.encodeWord {nX nA : ℕ} (u : FreeMonoid (FinGen nX nA)) : List Coded.Letter

The code of a word.

Equations

• MIPRE.Tsirelson.encodeWord u = List.map MIPRE.Tsirelson.encodeLetter (FreeMonoid.toList u)

@[simp]

theorem MIPRE.Tsirelson.decodeWord_nil {nX nA : ℕ} : decodeWord nX nA [] = 1

The empty coded word decodes to the empty word.

@[simp]

theorem MIPRE.Tsirelson.decodeWord_singleton {nX nA : ℕ} (l : Coded.Letter) : decodeWord nX nA [l] = FreeMonoid.of (decodeLetter nX nA l)

A one-letter coded word decodes to its letter.

theorem MIPRE.Tsirelson.decodeWord_append {nX nA : ℕ} (w w' : List Coded.Letter) : decodeWord nX nA (w ++ w') = decodeWord nX nA w * decodeWord nX nA w'

The decoding of words is multiplicative.

theorem MIPRE.Tsirelson.decodeWord_reverse {nX nA : ℕ} (w : List Coded.Letter) : decodeWord nX nA w.reverse = (decodeWord nX nA w).reverse

The decoding of words commutes with reversal.

theorem MIPRE.Tsirelson.decodeWord_eq_one_iff {nX nA : ℕ} {w : List Coded.Letter} : decodeWord nX nA w = 1 ↔ w = []

Only the empty coded word decodes to the empty word.

@[simp]

theorem MIPRE.Tsirelson.decodeWord_encodeWord {nX nA : ℕ} (u : FreeMonoid (FinGen nX nA)) : decodeWord nX nA (encodeWord u) = u

Decoding inverts the code of a word.

theorem MIPRE.Tsirelson.encodeWord_decodeWord {nX nA : ℕ} {w : List Coded.Letter} (h : Coded.ValidWord nX nA w) : encodeWord (decodeWord nX nA w) = w

On valid words, the code inverts the decoding.

theorem MIPRE.Tsirelson.validWord_encodeWord {nX nA : ℕ} (u : FreeMonoid (FinGen nX nA)) : Coded.ValidWord nX nA (encodeWord u)

The code of a word is valid.

theorem MIPRE.Tsirelson.decodeWord_injOn {nX nA : ℕ} {w w' : List Coded.Letter} (hw : Coded.ValidWord nX nA w) (hw' : Coded.ValidWord nX nA w') (h : decodeWord nX nA w = decodeWord nX nA w') : w = w'

The decoding is injective on valid words: the code is a left inverse there.

Decoding coded polynomials

noncomputable def MIPRE.Tsirelson.interp (nX nA : ℕ) (l : Coded.CPoly) : NCPoly (FinGen nX nA)

The decoding of a coded polynomial [(w, c), …]: the polynomial Σ c · w.

Equations

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

@[simp]

theorem MIPRE.Tsirelson.interp_nil {nX nA : ℕ} : interp nX nA [] = 0

The empty coded polynomial decodes to 0.

@[simp]

theorem MIPRE.Tsirelson.interp_cons {nX nA : ℕ} (m : List Coded.Letter × ValueApprox.GInt) (l : Coded.CPoly) : interp nX nA (m :: l) = NCPoly.single (decodeWord nX nA m.1) m.2.toC + interp nX nA l

The decoding, one monomial at a time.

theorem MIPRE.Tsirelson.interp_append {nX nA : ℕ} (p q : Coded.CPoly) : interp nX nA (p ++ q) = interp nX nA p + interp nX nA q

The decoding is additive.

theorem MIPRE.Tsirelson.interp_cneg {nX nA : ℕ} (p : Coded.CPoly) : interp nX nA (Coded.cneg p) = -interp nX nA p

The decoding of a coded negation.

theorem MIPRE.Tsirelson.interp_cscale {nX nA : ℕ} (c : ValueApprox.GInt) (p : Coded.CPoly) : interp nX nA (Coded.cscale c p) = c.toC • interp nX nA p

The decoding of a coded multiple.

theorem MIPRE.Tsirelson.interp_map_mul {nX nA : ℕ} (m : List Coded.Letter × ValueApprox.GInt) (q : Coded.CPoly) : interp nX nA (List.map (fun (m' : List Coded.Letter × ValueApprox.GInt) => (m.1 ++ m'.1, m.2.mul m'.2)) q) = NCPoly.single (decodeWord nX nA m.1) m.2.toC * interp nX nA q

The decoding of a monomial times a coded polynomial.

theorem MIPRE.Tsirelson.interp_cmul {nX nA : ℕ} (p q : Coded.CPoly) : interp nX nA (Coded.cmul p q) = interp nX nA p * interp nX nA q

The decoding is multiplicative.

theorem MIPRE.Tsirelson.interp_cstar {nX nA : ℕ} (p : Coded.CPoly) : interp nX nA (Coded.cstar p) = star (interp nX nA p)

The decoding commutes with the star.

theorem MIPRE.Tsirelson.interp_cconst {nX nA : ℕ} (c : ValueApprox.GInt) : interp nX nA (Coded.cconst c) = NCPoly.single 1 c.toC

The decoding of a coded constant.

theorem MIPRE.Tsirelson.interp_cword {nX nA : ℕ} (w : List Coded.Letter) : interp nX nA (Coded.cword w) = NCPoly.single (decodeWord nX nA w) 1

The decoding of a coded word with coefficient 1.

theorem MIPRE.Tsirelson.interp_optPoly {nX nA : ℕ} (g : Option Coded.Letter) : interp nX nA (Coded.optPoly g) = (Option.map (decodeLetter nX nA) g).elim 1 NCPoly.gen

The decoding of the polynomial of an optional letter: 1 or a generator.

theorem MIPRE.Tsirelson.interp_flatMap {nX nA : ℕ} {β : Type u_1} (l : List β) (f : β → Coded.CPoly) : interp nX nA (List.flatMap f l) = (List.map (fun (b : β) => interp nX nA (f b)) l).sum

The decoding of a concatenation of coded polynomials.

theorem MIPRE.Tsirelson.interp_map {nX nA : ℕ} {β : Type u_1} (l : List β) (f : β → List Coded.Letter × ValueApprox.GInt) : interp nX nA (List.map f l) = (List.map (fun (b : β) => NCPoly.single (decodeWord nX nA (f b).1) (f b).2.toC) l).sum

The decoding of a list of monomials.

theorem MIPRE.Tsirelson.sum_map_range {M : Type u_1} [AddCommMonoid M] (n : ℕ) (g : ℕ → M) : (List.map g (List.range n)).sum = ∑ i : Fin n, g ↑i

A sum over List.range n as a sum over Fin n.

Relations and the game polynomial

theorem MIPRE.Tsirelson.interp_aliceNorm {nX nA : ℕ} (x : ℕ) : interp nX nA (Coded.aliceNorm nA x) = ∑ a : Fin (nA + 1), eG (finOf nX x) a - 1

The first player's coded normalization decodes to Σ_a e_xa - 1.

theorem MIPRE.Tsirelson.interp_bobNorm {nX nA : ℕ} (y : ℕ) : interp nX nA (Coded.bobNorm nA y) = ∑ b : Fin (nA + 1), fG (finOf nX y) b - 1

The second player's coded normalization decodes to Σ_b f_yb - 1.

theorem MIPRE.Tsirelson.interp_commPoly {nX nA : ℕ} (t : ℕ × ℕ × ℕ × ℕ) : interp nX nA (Coded.commPoly t) = eG (finOf nX t.1) (finOf nA t.2.2.1) * fG (finOf nX t.2.1) (finOf nA t.2.2.2) - fG (finOf nX t.2.1) (finOf nA t.2.2.2) * eG (finOf nX t.1) (finOf nA t.2.2.1)

The coded commutator decodes to e_xa f_yb - f_yb e_xa.

theorem MIPRE.Tsirelson.interp_relPoly_mem {nX nA : ℕ} (ρ : Coded.RelIdx) : interp nX nA (Coded.relPoly nA ρ) ∈ FinRels nX nA

Every relation index decodes to a relation.

theorem MIPRE.Tsirelson.exists_relIdx {nX nA : ℕ} {ρ : NCPoly (FinGen nX nA)} (hρ : ρ ∈ FinRels nX nA) : ∃ (i : Coded.RelIdx), Coded.ValidRel nX nA i ∧ interp nX nA (Coded.relPoly nA i) = ρ

Every relation is the decoding of a valid relation index.

theorem MIPRE.Tsirelson.interp_Wint (d : HaltingGameValue.GameData) : interp d.nX d.nA (Coded.Wint d) = ↑(ValueApprox.W d) • gamePoly d.game

The coded game polynomial decodes to W_d times the game polynomial.

Coefficients and dominance

theorem MIPRE.Tsirelson.coeff_interp {nX nA : ℕ} {l : Coded.CPoly} (hl : Coded.ValidCPoly nX nA l) {w : List Coded.Letter} (hw : Coded.ValidWord nX nA w) : (interp nX nA l).coeff (decodeWord nX nA w) = (Coded.coeffRaw l w).toC

The merged coefficient of a valid word in a valid coded polynomial is the coefficient of its decoding.

theorem MIPRE.Tsirelson.support_interp_subset {nX nA : ℕ} [DecidableEq (FreeMonoid (FinGen nX nA))] (l : Coded.CPoly) : (interp nX nA l).coeff.support ⊆ Finset.image (decodeWord nX nA) (List.map Prod.fst l).toFinset

The support of the decoding lies in the decoded words.

theorem MIPRE.Tsirelson.isDominant_iff_dominant_interp {nX nA : ℕ} {l : Coded.CPoly} (hl : Coded.ValidCPoly nX nA l) : Coded.IsDominant l ↔ Dominant (interp nX nA l)

The coded dominance test is dominance of the decoding, for valid coded polynomials.

Decoded certificates

noncomputable def MIPRE.Tsirelson.decodeSos (nX nA : ℕ) (sos : List (Option Coded.Letter × Coded.CPoly)) : List (Option (FinGen nX nA) × NCPoly (FinGen nX nA))

The decoded hermitian squares of a certificate.

Equations

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

noncomputable def MIPRE.Tsirelson.decodeIdeal (nX nA : ℕ) (ideal : List (ValueApprox.GInt × List Coded.Letter × Coded.RelIdx × List Coded.Letter)) : List (ℂ × FreeMonoid (FinGen nX nA) × { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA } × FreeMonoid (FinGen nX nA))

The decoded ideal monomials of a certificate.

Equations

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

theorem MIPRE.Tsirelson.interp_sosSum {nX nA : ℕ} (sos : List (Option Coded.Letter × Coded.CPoly)) : interp nX nA (Coded.sosSum sos) = sosPoly (decodeSos nX nA sos)

The decoding of the coded hermitian squares of a certificate.

theorem MIPRE.Tsirelson.interp_idealSum {nX nA : ℕ} (ideal : List (ValueApprox.GInt × List Coded.Letter × Coded.RelIdx × List Coded.Letter)) : interp nX nA (Coded.idealSum nA ideal) = idealPoly (decodeIdeal nX nA ideal)

The decoding of the coded ideal monomials of a certificate.

theorem MIPRE.Tsirelson.interp_certR (d : HaltingGameValue.GameData) (p q : ℕ) (cert : Coded.Cert) : interp d.nX d.nA (Coded.certR d p q cert) = ↑(cert.1 * cert.1 * p * ValueApprox.W d) • 1 - ↑(cert.1 * cert.1 * q) • ↑(ValueApprox.W d) • gamePoly d.game - sosPoly (decodeSos d.nX d.nA cert.2.1) - idealPoly (decodeIdeal d.nX d.nA cert.2.2)

The decoded residual of a certificate.

theorem MIPRE.Tsirelson.interp_certR_eq (d : HaltingGameValue.GameData) (p : ℕ) {q : ℕ} (hq : q ≠ 0) (cert : Coded.Cert) : interp d.nX d.nA (Coded.certR d p q cert) = ↑cert.1 ^ 2 • ((↑q * ↑(ValueApprox.W d) * (↑p / ↑q)) • 1 - (↑q * ↑(ValueApprox.W d)) • gamePoly d.game) - sosPoly (decodeSos d.nX d.nA cert.2.1) - idealPoly (decodeIdeal d.nX d.nA cert.2.2)

The decoded residual of a certificate is the residual of Certificate, at κ = q·W_d and r = p / q.

theorem MIPRE.Tsirelson.interp_certRh (d : HaltingGameValue.GameData) (p q : ℕ) (cert : Coded.Cert) : interp d.nX d.nA (Coded.certRh d p q cert) = interp d.nX d.nA (Coded.certR d p q cert) + star (interp d.nX d.nA (Coded.certR d p q cert))

The decoded hermitian residual of a certificate.

Soundness

theorem MIPRE.Tsirelson.cast_W_pos (d : HaltingGameValue.GameData) : 0 < ↑(ValueApprox.W d)

The normalizing weight of a description is positive.

theorem MIPRE.Tsirelson.checkUpper_sound {d : HaltingGameValue.GameData} {p q : ℕ} {cert : Coded.Cert} (h : Coded.CheckUpper (d, p, q) cert) : commutingOperatorValue d.game < ↑p / ↑q

Soundness of the coded check: an accepted certificate for (d, p, q) bounds the commuting-operator value of d.game strictly below p / q.

Encoding certificates

noncomputable def MIPRE.Tsirelson.encodeC (z : ℂ) : ValueApprox.GInt

The code of a complex number, read off the floors of its parts; exact on Gaussian integers.

Equations

• MIPRE.Tsirelson.encodeC z = MIPRE.ValueApprox.GInt.ofInt ⌊z.re⌋ ⌊z.im⌋

theorem MIPRE.Tsirelson.toC_encodeC {z : ℂ} (h : ∃ (m : ℤ) (n : ℤ), z = ↑m + ↑n * Complex.I) : (encodeC z).toC = z

The code of a Gaussian integer is exact.

noncomputable def MIPRE.Tsirelson.encodePoly {nX nA : ℕ} (s : NCPoly (FinGen nX nA)) : Coded.CPoly

The code of a polynomial: its monomials, in the order of Finset.toList.

Equations

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

theorem MIPRE.Tsirelson.interp_encodePoly {nX nA : ℕ} {s : NCPoly (FinGen nX nA)} (hs : ∀ (w : FreeMonoid (FinGen nX nA)), ∃ (m : ℤ) (n : ℤ), s.coeff w = ↑m + ↑n * Complex.I) : interp nX nA (encodePoly s) = s

The code of a polynomial with Gaussian-integer coefficients is exact.

theorem MIPRE.Tsirelson.validCPoly_encodePoly {nX nA : ℕ} (s : NCPoly (FinGen nX nA)) : Coded.ValidCPoly nX nA (encodePoly s)

The code of a polynomial is valid.

noncomputable def MIPRE.Tsirelson.relIdxOf {nX nA : ℕ} (ρ : { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA }) : Coded.RelIdx

The code of a relation: a valid relation index decoding to it.

Equations

• MIPRE.Tsirelson.relIdxOf ρ = Classical.choose ⋯

theorem MIPRE.Tsirelson.validRel_relIdxOf {nX nA : ℕ} (ρ : { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA }) : Coded.ValidRel nX nA (relIdxOf ρ)

The code of a relation is valid.

theorem MIPRE.Tsirelson.interp_relPoly_relIdxOf {nX nA : ℕ} (ρ : { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA }) : interp nX nA (Coded.relPoly nA (relIdxOf ρ)) = ↑ρ

The code of a relation decodes to it.

noncomputable def MIPRE.Tsirelson.encodeSos {nX nA : ℕ} (σ : List (Option (FinGen nX nA) × NCPoly (FinGen nX nA))) : List (Option Coded.Letter × Coded.CPoly)

The code of a list of hermitian squares.

Equations

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

noncomputable def MIPRE.Tsirelson.encodeIdeal {nX nA : ℕ} (ι : List (ℂ × FreeMonoid (FinGen nX nA) × { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA } × FreeMonoid (FinGen nX nA))) : List (ValueApprox.GInt × List Coded.Letter × Coded.RelIdx × List Coded.Letter)

The code of a list of ideal monomials.

Equations

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

theorem MIPRE.Tsirelson.decodeSos_encodeSos {nX nA : ℕ} {σ : List (Option (FinGen nX nA) × NCPoly (FinGen nX nA))} (hσ : ∀ t ∈ σ, ∀ (w : FreeMonoid (FinGen nX nA)), ∃ (m : ℤ) (n : ℤ), t.2.coeff w = ↑m + ↑n * Complex.I) : decodeSos nX nA (encodeSos σ) = σ

The code of hermitian squares with Gaussian-integer coefficients is exact.

theorem MIPRE.Tsirelson.decodeIdeal_encodeIdeal {nX nA : ℕ} {ι : List (ℂ × FreeMonoid (FinGen nX nA) × { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA } × FreeMonoid (FinGen nX nA))} (hι : ∀ t ∈ ι, ∃ (m : ℤ) (n : ℤ), t.1 = ↑m + ↑n * Complex.I) : decodeIdeal nX nA (encodeIdeal ι) = ι

The code of ideal monomials with Gaussian-integer coefficients is exact.

theorem MIPRE.Tsirelson.validCert_encode {nX nA : ℕ} (N : ℕ) (σ : List (Option (FinGen nX nA) × NCPoly (FinGen nX nA))) (ι : List (ℂ × FreeMonoid (FinGen nX nA) × { ρ : NCPoly (FinGen nX nA) // ρ ∈ FinRels nX nA } × FreeMonoid (FinGen nX nA))) : Coded.ValidCert nX nA (N, encodeSos σ, encodeIdeal ι)

The code of a certificate is valid.

Completeness

theorem MIPRE.Tsirelson.checkUpper_complete {d : HaltingGameValue.GameData} {p q : ℕ} (h : commutingOperatorValue d.game < ↑p / ↑q) : ∃ (cert : Coded.Cert), Coded.CheckUpper (d, p, q) cert

Completeness of the coded check: if the commuting-operator value of d.game is strictly below p / q, some certificate for (d, p, q) is accepted.

theorem MIPRE.Tsirelson.checkUpper_iff (x : HaltingGameValue.GameData × ℕ × ℕ) : (∃ (cert : Coded.Cert), Coded.CheckUpper x cert) ↔ commutingOperatorValue x.1.game < ↑x.2.1 / ↑x.2.2

The coded check characterizes the thresholds above the commuting-operator value.

theorem MIPRE.commutingUpperRE : CommutingUpperRE

The commuting-operator value is recursively enumerable from above (blueprint lem:valco-upper-re): the triples (d, p, q) with valco(G_d) < p / q form an r.e. set. The semidecider searches for a certificate accepted by the primitive recursive check Tsirelson.Coded.CheckUpper.

theorem MIPRE.ValueModel.commuting_upperRE : commuting.UpperRE

The commuting-operator value is r.e. from above, as a property of the value model ValueModel.commuting: lem:valco-upper-re in the vocabulary the halting reduction of MIP^co = coRE consumes.

theorem MIPRE.tsirelson_of_haltingReduction (hred : HaltingReductionQuantum) : ∃ (nX : ℕ) (nA : ℕ), Cqa (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1)) ⊂ Cqc (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))

Tsirelson's problem, negative answer, given the halting reduction (blueprint cor:tsirelson): C_qa ⊊ C_qc in some finite scenario with equal question alphabets Fin (nX + 1) and equal answer alphabets Fin (nA + 1) for both players.