An explicit separation of the quantum and commuting-operator values

Blueprint thm:separation (planning/explicit-separation.md): a described game G with val*(G) ≤ 1/2 and ω_co(G) = 1, and a commuting-operator correlation of payoff 1 that lies outside C_qa. Both analytic inputs are hypotheses here, as in MIPRE.Foundations.Tsirelson. Conditional: the halting reduction HaltingReductionQuantum and the upper semidecider CommutingUpperRE. MIPRE/Tsirelson.lean discharges them.

The fixed point (exists_quantumValue_le_half_commutingOperatorValue_eq_one). Let g be the halting reduction. The predicate c ↦ ω_co(g c) < 1 is r.e., so Kleene's recursion theorem (Nat.Partrec.Code.fixed_point₂) gives a code e that halts on the empty input exactly when ω_co(g e) < 1. If e halted, then val*(g e) = 1, so ω_co(g e) = 1 and e would not halt. So e does not halt: val*(g e) ≤ 1/2, and ω_co(g e) = 1 because it is not below 1. The game is g e, uniform in the codes of g and of the semidecider. Unlike the paper's G^sep, nothing about entanglement is needed: the case ω_co = 1 is the non-halting case of the reduction, whose soundness is already the value-form compression chain.

The correlation (exists_mem_Cqc_payoff_eq_commutingOperatorValue). The payoff is continuous and C_qc is compact and nonempty, so the payoff attains its maximum on C_qc, and the maximum is the commuting-operator value. For the game above, that correlation has payoff 1, and it is outside C_qa, where payoffs are at most val* ≤ 1/2.

Main declarations

• exists_mem_Cqc_payoff_eq_commutingOperatorValue;
• exists_quantumValue_le_half_commutingOperatorValue_eq_one;
• separation_of_upperRE.

theorem MIPRE.exists_mem_Cqc_payoff_eq_commutingOperatorValue {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) : ∃ p ∈ Cqc X Y A B, G.payoff p = commutingOperatorValue G

The commuting-operator value is attained on C_qc: some commuting-operator correlation has payoff exactly ω_co(G), since the payoff is continuous and C_qc is compact.

theorem MIPRE.exists_quantumValue_le_half_commutingOperatorValue_eq_one (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) : ∃ (d : HaltingGameValue.GameData), quantumValue d.game ≤ 1 / 2 ∧ commutingOperatorValue d.game = 1

The fixed-point game: given the halting reduction and an upper semidecider for the commuting-operator value, some described game has quantum value at most 1/2 and commuting-operator value 1.

theorem MIPRE.separation_of_upperRE (hred : HaltingReductionQuantum) (hU : CommutingUpperRE) : ∃ (d : HaltingGameValue.GameData), quantumValue d.game ≤ 1 / 2 ∧ commutingOperatorValue d.game = 1 ∧ ∃ p ∈ Cqc (Fin (d.nX + 1)) (Fin (d.nX + 1)) (Fin (d.nA + 1)) (Fin (d.nA + 1)), d.game.payoff p = 1 ∧ p ∉ Cqa (Fin (d.nX + 1)) (Fin (d.nX + 1)) (Fin (d.nA + 1)) (Fin (d.nA + 1))

The explicit separation, given an upper semidecider (blueprint thm:separation): given the halting reduction and an upper semidecider for the commuting-operator value, some described game G has val*(G) ≤ 1/2 and ω_co(G) = 1, and some commuting-operator correlation in its scenario has payoff 1 and lies outside C_qa.