Tsirelson's problem from an upper semidecider for the commuting-operator value

The non-explicit route to the negative answer to Tsirelson's problem (blueprint cor:tsirelson), with its two analytic inputs as explicit hypotheses:

• CommutingUpperRE: the commuting-operator value is recursively enumerable from above, in the threshold encoding of MIPRE.ValueApprox.rePred_lt_quantumValue (a pair (p, q) stands for p / q, and p / 0 = 0);
• closedness of C_qc in every finite scenario.

The halting reduction of cor:main-quantum (MIPRE.Halting.halting_reduction_quantum) enters as the hypothesis hred, whose type is that theorem's statement: it lives in the root module MIPRE.MainTheorem, which MIPRE/Foundations/ does not import.

The argument (exists_quantumValue_lt_commutingOperatorValue): if the two values agreed on every described game, a machine would fail to halt exactly when the commuting-operator value of its game is below 3/4 (the quantum value is 1 or at most 1/2), so non-halting would be r.e., which it is not (ComputablePred.halting_problem_not_re). A game whose commuting-operator value exceeds its quantum value has a commuting-operator strategy that beats the quantum value, and its correlation lies outside C_qa, since payoffs on C_qa are bounded by the quantum value (exists_mem_Cqc_not_mem_Cqa). With C_qc closed, C_qa ⊆ C_qc, and the inclusion is strict (tsirelson_of_upperRE_of_isClosed).

Main declarations

• HaltingReductionQuantum, CommutingUpperRE;
• exists_quantumValue_lt_commutingOperatorValue, exists_mem_Cqc_not_mem_Cqa, exists_Cqa_ne_Cqc, tsirelson_of_upperRE_of_isClosed.

@[reducible, inline]

abbrev MIPRE.HaltingReductionQuantum : Prop

The halting reduction of cor:main-quantum, as a proposition: a computable map from codes to game descriptions whose quantum value is 1 on halting codes and at most 1/2 on the others. MIPRE.Halting.halting_reduction_quantum proves it.

Equations

• MIPRE.HaltingReductionQuantum = MIPRE.ValueModel.tensor.HaltingReductionRE

@[reducible, inline]

abbrev MIPRE.CommutingUpperRE : Prop

The commuting-operator value is r.e. from above (blueprint lem:valco-upper-re): the pairs (d, p, q) with valco(G_d) < p / q form an r.e. set. The threshold encoding is that of the lower semidecider MIPRE.ValueApprox.rePred_lt_quantumValue.

Equations

• MIPRE.CommutingUpperRE = MIPRE.ValueModel.commuting.UpperRE

theorem MIPRE.exists_quantumValue_lt_commutingOperatorValue (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) : ∃ (d : HaltingGameValue.GameData), quantumValue d.game < commutingOperatorValue d.game

The two values differ on some described game, given the halting reduction and an upper semidecider for the commuting-operator value.

theorem MIPRE.exists_mem_Cqc_not_mem_Cqa (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) : ∃ (nX : ℕ) (nA : ℕ), ∃ p ∈ Cqc (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1)), p ∉ Cqa (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))

A commuting-operator correlation outside C_qa, in the scenario of a described game, given the halting reduction and an upper semidecider for the commuting-operator value.

theorem MIPRE.exists_Cqa_ne_Cqc (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) : ∃ (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))

C_qa ≠ C_qc in some finite scenario, given the halting reduction and an upper semidecider for the commuting-operator value.

theorem MIPRE.tsirelson_of_upperRE_of_isClosed (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) (hclosed : ∀ (nX nA : ℕ), IsClosed (Cqc (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1)))) : ∃ (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, conditionally (blueprint cor:tsirelson): C_qa ⊊ C_qc in some finite scenario, given the halting reduction, an upper semidecider for the commuting-operator value, and closedness of C_qc. The scenario has equal question alphabets Fin (nX + 1) and equal answer alphabets Fin (nA + 1) for both players.