The Magic Square as a nonlocal game

MIPRE.LCS.MagicSquare.game is the Mermin--Peres magic square as an LCS instance; nonlocalGame is the two-player game it induces through MIPRE.LCS.Game.toNonlocalGame, which is what blueprint lem:ms-direct-anticomm and the Pauli basis test's Magic Square subtest are about.

The point of this file is the non-vacuity witnesses. A decider that accepts everything, or rejects everything, makes every soundness statement about the game either false or empty, and that is not a hypothetical: reports/clgame-format-check-missing.md records the seeded CL game's missing format check doing exactly that. So each of the four possibilities is pinned here by decide on explicit answers:

• an oriented pair that is accepted (accepts_zero), in both orientations;
• one that is rejected because the bits disagree (rejects_disagree);
• one that is rejected because the assignment violates its equation (rejects_unsatisfied) --- note this one has the bits agreeing, so it isolates the parity check;
• one that is rejected because an answer has the wrong shape (rejects_shape).

layout.V 5 = {2, 5, 8} carries the odd right-hand side, so rejects_odd_column also checks that the parity actually reads game.b rather than always testing against zero.

theorem MIPRE.LCS.MagicSquare.r_pos : 0 < layout.r

The magic square has six equations.

theorem MIPRE.LCS.MagicSquare.V_nonempty (i : Fin layout.r) : (layout.V i).Nonempty

Every equation of the magic square has a nonempty support.

noncomputable def MIPRE.LCS.MagicSquare.nonlocalGame : MIPRE.Game layout.Question layout.Question layout.Answer layout.Answer

The Magic Square as a nonlocal game.

Equations

• MIPRE.LCS.MagicSquare.nonlocalGame = MIPRE.LCS.MagicSquare.game.toNonlocalGame MIPRE.LCS.MagicSquare.r_pos MIPRE.LCS.MagicSquare.V_nonempty

Non-vacuity

The all-zero assignment satisfies equation 0 (whose right-hand side is 0), so with the matching bit it is accepted; changing the bit, or the assignment's parity, is rejected.

def MIPRE.LCS.MagicSquare.v (k : ℕ) (h : k < layout.s := by decide) : Fin layout.s

A variable index, written as a numeral. layout.s is not a literal, so the OfNat instance does not fire.

Equations

• MIPRE.LCS.MagicSquare.v k h = ⟨k, h⟩

def MIPRE.LCS.MagicSquare.e (k : ℕ) (h : k < layout.r := by decide) : Fin layout.r

An equation index, written as a numeral.

Equations

• MIPRE.LCS.MagicSquare.e k h = ⟨k, h⟩

def MIPRE.LCS.MagicSquare.zeroAssign : Fin layout.s → ZMod 2

The all-zero assignment.

Equations

• MIPRE.LCS.MagicSquare.zeroAssign x✝ = 0

def MIPRE.LCS.MagicSquare.oneAt (k : Fin layout.s) : Fin layout.s → ZMod 2

The assignment that is 1 at variable k and 0 elsewhere.

Equations

• MIPRE.LCS.MagicSquare.oneAt k l = if l = k then 1 else 0

theorem MIPRE.LCS.MagicSquare.accepts_zero : game.accepts (Sum.inl (e 0 accepts_zero._proof_1)) (Sum.inr (v 0 accepts_zero._proof_2)) (Sum.inl zeroAssign) (Sum.inr 0) = true

theorem MIPRE.LCS.MagicSquare.accepts_zero_swapped : game.accepts (Sum.inr (v 0 accepts_zero._proof_2)) (Sum.inl (e 0 accepts_zero._proof_1)) (Sum.inr 0) (Sum.inl zeroAssign) = true

theorem MIPRE.LCS.MagicSquare.rejects_disagree : game.accepts (Sum.inl (e 0 accepts_zero._proof_1)) (Sum.inr (v 0 accepts_zero._proof_2)) (Sum.inl zeroAssign) (Sum.inr 1) = false

theorem MIPRE.LCS.MagicSquare.rejects_unsatisfied : game.accepts (Sum.inl (e 0 accepts_zero._proof_1)) (Sum.inr (v 0 accepts_zero._proof_2)) (Sum.inl (oneAt (v 0 accepts_zero._proof_2))) (Sum.inr 1) = false

theorem MIPRE.LCS.MagicSquare.rejects_shape : game.accepts (Sum.inl (e 0 accepts_zero._proof_1)) (Sum.inr (v 0 accepts_zero._proof_2)) (Sum.inr 0) (Sum.inl zeroAssign) = false

theorem MIPRE.LCS.MagicSquare.rejects_odd_column : game.accepts (Sum.inl (e 5 rejects_odd_column._proof_1)) (Sum.inr (v 2 rejects_odd_column._proof_2)) (Sum.inl zeroAssign) (Sum.inr 0) = false

The last column has right-hand side 1, so the all-zero assignment fails it: the parity check reads game.b and does not always test against zero.

theorem MIPRE.LCS.MagicSquare.accepts_odd_column : game.accepts (Sum.inl (e 5 rejects_odd_column._proof_1)) (Sum.inr (v 2 rejects_odd_column._proof_2)) (Sum.inl (oneAt (v 2 rejects_odd_column._proof_2))) (Sum.inr 1) = true

... and the assignment that is 1 at variable 2 alone does satisfy it.

theorem MIPRE.LCS.MagicSquare.rejects_off_support : game.accepts (Sum.inl (e 0 accepts_zero._proof_1)) (Sum.inr (v 3 rejects_off_support._proof_1)) (Sum.inl zeroAssign) (Sum.inr 0) = false

An off-support incidence is rejected: variable 3 does not occur in equation 0.

The cells of a constraint

The magic square's six equations are the three rows and the three columns, in that order, so the j-th cell of equation c is 3c + j for a row and 3j + (c - 3) for a column.

def MIPRE.LCS.MagicSquare.cellNat (c j : ℕ) : ℕ

The index of the j-th cell of the c-th equation.

Equations

• MIPRE.LCS.MagicSquare.cellNat c j = if c < 3 then 3 * c + j else 3 * j + (c - 3)

def MIPRE.LCS.MagicSquare.cell (c : Fin layout.r) (j : Fin 3) : Fin layout.s

The j-th cell of constraint c.

Equations

• MIPRE.LCS.MagicSquare.cell c j = ⟨MIPRE.LCS.MagicSquare.cellNat ↑c ↑j, ⋯⟩

theorem MIPRE.LCS.MagicSquare.V_eq_cells (c : Fin layout.r) : layout.V c = {cell c 0, cell c 1, cell c 2}

theorem MIPRE.LCS.MagicSquare.cell_ne_01 (c : Fin layout.r) : cell c 0 ≠ cell c 1

theorem MIPRE.LCS.MagicSquare.cell_ne_02 (c : Fin layout.r) : cell c 0 ≠ cell c 2

theorem MIPRE.LCS.MagicSquare.cell_ne_12 (c : Fin layout.r) : cell c 1 ≠ cell c 2

theorem MIPRE.LCS.MagicSquare.cell_mem (c : Fin layout.r) (j : Fin 3) : cell c j ∈ layout.V c

theorem MIPRE.LCS.MagicSquare.sum_cells (c : Fin layout.r) (a : Fin layout.s → ZMod 2) : ∑ k ∈ layout.V c, a k = a (cell c 0) + a (cell c 1) + a (cell c 2)

A sum over a constraint's support is the sum over its three cells.

def MIPRE.LCS.MagicSquare.cellIdx (c : Fin layout.r) (j : Fin layout.s) : Fin 3

The position of the variable j within the support of constraint c, the inverse of cell c; junk (2) for a variable outside the support.

Equations

• MIPRE.LCS.MagicSquare.cellIdx c j = if MIPRE.LCS.MagicSquare.cell c 0 = j then 0 else if MIPRE.LCS.MagicSquare.cell c 1 = j then 1 else 2

theorem MIPRE.LCS.MagicSquare.cell_cellIdx {c : Fin layout.r} {j : Fin layout.s} (h : j ∈ layout.V c) : cell c (cellIdx c j) = j

@[simp]

theorem MIPRE.LCS.MagicSquare.cellIdx_cell (c : Fin layout.r) (k : Fin 3) : cellIdx c (cell c k) = k