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 ObservableStrategyData.

Types

@[reducible, inline]

abbrev mat4 : Type

The 4×4 matrix type used for two-qubit observables in the magic square construction.

Equations

• mat4 = Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

@[reducible, inline]

abbrev mat16 : Type

The 16×16 matrix type used for the bipartite lift of the two-qubit strategy.

Equations

• mat16 = Matrix ((Fin 2 × Fin 2) × Fin 2 × Fin 2) ((Fin 2 × Fin 2) × Fin 2 × Fin 2) ℂ

Layout

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

def magic_square_layout : LCSLayout

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 magic_square_game : LCSGame magic_square_layout

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

Equations

• magic_square_game = { b := fun (i : Fin magic_square_layout.r) => if i = ⟨5, magic_square_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 magic_square_grid : Fin 9 → mat4

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

Equations

• magic_square_grid 0 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X I2
• magic_square_grid 1 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) I2 X
• magic_square_grid 2 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X X
• magic_square_grid 3 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) I2 Y
• magic_square_grid 4 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y I2
• magic_square_grid 5 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y Y
• magic_square_grid 6 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X Y
• magic_square_grid 7 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y X
• magic_square_grid 8 = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Z Z

theorem magic_square_is_observable (j : Fin 9) : IsObservable (magic_square_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 tacticSolve_line_comm : Lean.ParserDescr

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

Equations

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

theorem MP_sameEquation_comm (i : Fin 6) : Pairwise fun (j k : ↥(magic_square_layout.V i)) => Commute (magic_square_grid ↑j) (magic_square_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 Strat_merminPeres : ObservableStrategyData mat16 magic_square_layout

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

Equations

• Strat_merminPeres = BipartiteObservableStrategy magic_square_grid magic_square_is_observable MP_sameEquation_comm