The Magic Square game has a perfect ZPC strategy

Paper II, Examples 2.13–2.14 (II:1300–1370): the Mermin–Peres Magic Square, as a linear constraint system game tailored with all variables unreadable, has a perfect Z-aligned permutation strategy commuting along edges, on the signed set (F₂²)_± of eight points — while the system itself has no solution, so the game has no perfect classical strategy, and no perfect ZPC strategy when tailored with all variables readable (Remark II:1250). This is the non-vacuity witness of plan §5, Phase 1: perfect ZPC strategies are not classical strategies in disguise.

• game: the questions are the six constraints (rows (false, r), columns (true, c)) and the nine cells; an edge joins a constraint to one of its three cells, with weight 1/18; each edge checks consistency (a_t = b) and the constraint (a₀ + a₁ + a₂ = parity, rows 0, columns 1) as two linear constraints.
• obs: the paper's grid of signed permutations of F₂² ≅ Fin 4 (II:1363), built from the bit flip pX and the conditional sign flip pZ on one bit. Its group identities — involutions, commuting along rows and columns, rows multiplying to Id and columns to -Id — are checked by decide, in the group SignedPerm (Fin 4), and transported to matrices by SignedPerm.toMatrixHom.
• strategy, value_strategy: the perfect ZPC strategy; hasPerfectZPC, and through the doubled game valStar_eq_one.

The game

@[reducible, inline]

abbrev MIPRE.Tailored.MagicSquare.Cons : Type

The constraints: rows (false, r) and columns (true, c).

Equations

• MIPRE.Tailored.MagicSquare.Cons = (Bool × Fin 3)

@[reducible, inline]

abbrev MIPRE.Tailored.MagicSquare.Var : Type

The variables: the cells of the grid.

Equations

• MIPRE.Tailored.MagicSquare.Var = (Fin 3 × Fin 3)

@[reducible, inline]

abbrev MIPRE.Tailored.MagicSquare.Question : Type

The questions: a constraint, or a cell.

Equations

• MIPRE.Tailored.MagicSquare.Question = (MIPRE.Tailored.MagicSquare.Cons ⊕ MIPRE.Tailored.MagicSquare.Var)

def MIPRE.Tailored.MagicSquare.cell (c : Cons) (t : Fin 3) : Var

The t-th cell of a constraint.

Equations

• MIPRE.Tailored.MagicSquare.cell c t = if c.1 = true then (t, c.2) else (c.2, t)

def MIPRE.Tailored.MagicSquare.parity (c : Cons) : Bool

The parity of a constraint: rows sum to 0, columns to 1 (II:1342).

Equations

• MIPRE.Tailored.MagicSquare.parity c = c.1

def MIPRE.Tailored.MagicSquare.isEdge : Question → Question → Bool

An edge joins a constraint to one of its cells.

Equations

• MIPRE.Tailored.MagicSquare.isEdge (Sum.inl c) (Sum.inr v) = (List.finRange 3).any fun (t : Fin 3) => MIPRE.Tailored.MagicSquare.cell c t == v
• MIPRE.Tailored.MagicSquare.isEdge x✝¹ x✝ = false

theorem MIPRE.Tailored.MagicSquare.isEdge_iff {x y : Question} : isEdge x y = true ↔ ∃ (c : Cons) (t : Fin 3), x = Sum.inl c ∧ y = Sum.inr (cell c t)

def MIPRE.Tailored.MagicSquare.lenL : Question → ℕ

The number of linear variables: three at a constraint, one at a cell.

Equations

• MIPRE.Tailored.MagicSquare.lenL (Sum.inl val) = 3
• MIPRE.Tailored.MagicSquare.lenL (Sum.inr val) = 1

def MIPRE.Tailored.MagicSquare.edgeConstraints (c : Cons) (v : Var) : List Cost.BitStr

The two constraints of an edge (c, v), over the variables of c, of v, and J: consistency, a_t + b = 0 for the position t of v in c; and the constraint itself, a₀ + a₁ + a₂ + parity = 0.

Equations

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

theorem MIPRE.Tailored.MagicSquare.card_edges : (∑ x : Question, ∑ y : Question, if isEdge x y = true then 1 else 0) = 18

noncomputable def MIPRE.Tailored.MagicSquare.game : TailoredGame Question

The Magic Square game (II:1335), tailored with all variables unreadable (II:1310).

Equations

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

theorem MIPRE.Tailored.MagicSquare.game_len_inl (c : Cons) : game.len (Sum.inl c) = 3

theorem MIPRE.Tailored.MagicSquare.game_len_inr (v : Var) : game.len (Sum.inr v) = 1

theorem MIPRE.Tailored.MagicSquare.edge_of_pos {x y : Question} (h : 0 < game.μ x y) : ∃ (c : Cons) (t : Fin 3), x = Sum.inl c ∧ y = Sum.inr (cell c t)

The strategy

def MIPRE.Tailored.MagicSquare.pX : SignedPerm (Fin 2)

The bit flip X on one bit.

Equations

• MIPRE.Tailored.MagicSquare.pX = { perm := Equiv.swap 0 1, sign := fun (x : Fin 2) => false }

def MIPRE.Tailored.MagicSquare.pZ : SignedPerm (Fin 2)

The conditional sign flip Z on one bit.

Equations

• MIPRE.Tailored.MagicSquare.pZ = { perm := 1, sign := fun (i : Fin 2) => decide (i = 1) }

def MIPRE.Tailored.MagicSquare.two (g h : SignedPerm (Fin 2)) : SignedPerm (Fin 4)

g ⊗ h on two bits, as a signed permutation of Fin 4.

Equations

• MIPRE.Tailored.MagicSquare.two g h = MIPRE.Tailored.SignedPerm.map finProdFinEquiv (g.prod h)

def MIPRE.Tailored.MagicSquare.obs (v : Var) : SignedPerm (Fin 4)

The paper's grid (II:1363): X ⊗ I, I ⊗ X, XX; I ⊗ Z, Z ⊗ I, ZZ; and minus the products of the first two rows' cells.

Equations

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

theorem MIPRE.Tailored.MagicSquare.obs_mul_self (v : Var) : obs v * obs v = 1

theorem MIPRE.Tailored.MagicSquare.obs_comm (c : Cons) (t t' : Fin 3) : obs (cell c t) * obs (cell c t') = obs (cell c t') * obs (cell c t)

theorem MIPRE.Tailored.MagicSquare.obs_consistency (c : Cons) (t : Fin 3) : (List.map (fun (i : Fin 3) => if decide (cell c i = cell c t) = true then obs (cell c i) else 1) (List.finRange 3)).prod * (List.map (fun (x : Fin 1) => if true = true then obs (cell c t) else 1) (List.finRange 1)).prod = 1

The two linear constraints of each edge, as identities between signed permutations: consistency squares a cell's observable to Id; the rows multiply to Id and the columns to -Id.

theorem MIPRE.Tailored.MagicSquare.obs_parity (c : Cons) (t : Fin 3) : (List.map (fun (i : Fin 3) => if true = true then obs (cell c i) else 1) (List.finRange 3)).prod * (List.map (fun (x : Fin 1) => if false = true then obs (cell c t) else 1) (List.finRange 1)).prod = if parity c = true then SignedPerm.negOne else 1

def MIPRE.Tailored.MagicSquare.obsAt (x : Question) : Fin (game.len x) → SignedPerm (Fin 4)

The observables at each question.

Equations

• MIPRE.Tailored.MagicSquare.obsAt (Sum.inl val) = fun (i : Fin (MIPRE.Tailored.MagicSquare.game.len (Sum.inl val))) => MIPRE.Tailored.MagicSquare.obs (MIPRE.Tailored.MagicSquare.cell val i)
• MIPRE.Tailored.MagicSquare.obsAt (Sum.inr val) = fun (x : Fin (MIPRE.Tailored.MagicSquare.game.len (Sum.inr val))) => MIPRE.Tailored.MagicSquare.obs val

theorem MIPRE.Tailored.MagicSquare.obsAt_mul_self (x : Question) (i : Fin (game.len x)) : obsAt x i * obsAt x i = 1

theorem MIPRE.Tailored.MagicSquare.obsAt_comm (x : Question) (i j : Fin (game.len x)) : obsAt x i * obsAt x j = obsAt x j * obsAt x i

noncomputable def MIPRE.Tailored.MagicSquare.strategy : PermStrategy game

The perfect ZPC strategy (II:1362): every variable is unreadable, so Z-alignment is vacuous.

Equations

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

theorem MIPRE.Tailored.MagicSquare.obsChar_toMatrix {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {k : ℕ} (g : Fin k → SignedPerm Ω) (α : Fin k → Bool) : obsChar (fun (i : Fin k) => (g i).toMatrix) α = (List.map (fun (i : Fin k) => if α i = true then g i else 1) (List.finRange k)).prod.toMatrix

The observable of a linear constraint of signed permutation observables is the matrix of the product of the signed permutations.

theorem MIPRE.Tailored.MagicSquare.toMatrix_ite_negOne {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (γ : Bool) : (if γ = true then SignedPerm.negOne else 1).toMatrix = bitSign γ • 1

theorem MIPRE.Tailored.MagicSquare.value_strategy : strategy.value = 1

The strategy is perfect.

theorem MIPRE.Tailored.MagicSquare.hasPerfectZPC : game.HasPerfectZPC

The Magic Square game has a perfect ZPC strategy (II:1352).

theorem MIPRE.Tailored.MagicSquare.valStar_eq_one : game.valStar = 1

Hence its quantum value is 1, through the doubled game (lem:zpc-pcc).