Mermin-Peres Magic Square Game Strategy

This module defines the layout for the Mermin-Peres magic square Linear Constraint System (LCS) game and provides a valid quantum strategy for it using observables.

It verifies the commutativity requirements (both local within equations and global bipartite commutativity) necessary to define a valid ObservableStrategy.

Layout

This section defines the layout/geometry of the Mermin-Peres magic square game.

def MIPRE.LCS.MagicSquare.layout : Layout

The layout of the Mermin-Peres magic square game. It consists of 6 equations (3 rows and 3 columns) over 9 variables (the cells of the 3x3 grid).

Equations

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

def MIPRE.LCS.MagicSquare.game : Game layout

The support-style magic square game, with the final column equation having odd parity.

Equations

• MIPRE.LCS.MagicSquare.game = { b := fun (i : Fin MIPRE.LCS.MagicSquare.layout.r) => if i = ⟨5, MIPRE.LCS.MagicSquare.game._proof_1⟩ then 1 else 0 }

Grid

This section defines a strategy for the game from the previous section, given as a grid of observables.

def MIPRE.LCS.MagicSquare.grid : Fin 9 → Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The 9 observables for the Mermin-Peres magic square, defined as Kronecker products of Pauli matrices (X, Y, Z) and the identity (I).

Equations

• MIPRE.LCS.MagicSquare.grid 0 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.X MIPRE.LCS.Pauli.I
• MIPRE.LCS.MagicSquare.grid 1 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.I MIPRE.LCS.Pauli.X
• MIPRE.LCS.MagicSquare.grid 2 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.X MIPRE.LCS.Pauli.X
• MIPRE.LCS.MagicSquare.grid 3 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.I MIPRE.LCS.Pauli.Y
• MIPRE.LCS.MagicSquare.grid 4 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.Y MIPRE.LCS.Pauli.I
• MIPRE.LCS.MagicSquare.grid 5 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.Y MIPRE.LCS.Pauli.Y
• MIPRE.LCS.MagicSquare.grid 6 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.X MIPRE.LCS.Pauli.Y
• MIPRE.LCS.MagicSquare.grid 7 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.Y MIPRE.LCS.Pauli.X
• MIPRE.LCS.MagicSquare.grid 8 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) MIPRE.LCS.Pauli.Z MIPRE.LCS.Pauli.Z

theorem MIPRE.LCS.MagicSquare.isObservable_grid (j : Fin 9) : IsObservable (grid j)

Each observable in the Mermin-Peres grid is a self-adjoint involution.

Commutativity

This section proves the commutativity properties of the magic square grid.

These properties are required for the strategy to be valid.

def MIPRE.LCS.MagicSquare.tacticSolve_line_comm : Lean.ParserDescr

A tactic for proving pairwise commutativity within one row or column of the square.

Equations

• MIPRE.LCS.MagicSquare.tacticSolve_line_comm = Lean.ParserDescr.node `MIPRE.LCS.MagicSquare.tacticSolve_line_comm 1024 (Lean.ParserDescr.nonReservedSymbol "solve_line_comm" false)

theorem MIPRE.LCS.MagicSquare.row1_comm : Pairwise fun (j k : ↥(layout.V 0)) => Commute (grid ↑j) (grid ↑k)

Helper lemmas establishing pairwise commutativity for each row and column.

theorem MIPRE.LCS.MagicSquare.row2_comm : Pairwise fun (j k : ↥(layout.V 1)) => Commute (grid ↑j) (grid ↑k)

theorem MIPRE.LCS.MagicSquare.row3_comm : Pairwise fun (j k : ↥(layout.V 2)) => Commute (grid ↑j) (grid ↑k)

theorem MIPRE.LCS.MagicSquare.col1_comm : Pairwise fun (j k : ↥(layout.V 3)) => Commute (grid ↑j) (grid ↑k)

theorem MIPRE.LCS.MagicSquare.col2_comm : Pairwise fun (j k : ↥(layout.V 4)) => Commute (grid ↑j) (grid ↑k)

theorem MIPRE.LCS.MagicSquare.col3_comm : Pairwise fun (j k : ↥(layout.V 5)) => Commute (grid ↑j) (grid ↑k)

theorem MIPRE.LCS.MagicSquare.grid_sameEquation_comm (i : Fin 6) : Pairwise fun (j k : ↥(layout.V i)) => Commute (grid ↑j) (grid ↑k)

For every equation of the layout, the associated grid observables commute pairwise.

Strategy

This section shows that the grid strategy is a valid strategy for the magic square game.

noncomputable def MIPRE.LCS.MagicSquare.merminPeresStrategy : BipartiteObservableStrategy (Fin 2 × Fin 2) layout

The Mermin-Peres strategy for the magic square game. This strategy uses BipartiteObservableStrategy to lift the 9 grid observables to a valid bipartite observable strategy on a 16x16 space. It relies on grid_sameEquation_comm to satisfy the commutativity constraints for each equation.

Equations

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