Magic Square Solution Group

This module builds the binary linear system of the Mermin-Peres magic square game from its layout/game data and attaches the generic SolutionGroup construction.

The #eval commands below print the matrix rows, right-hand side, and equation supports so the finite presentation can be inspected directly.

def magic_square_system : LinearSystem

The explicit binary linear system underlying the Mermin-Peres magic square game.

Equations

• magic_square_system = magic_square_game.toLinearSystem

@[reducible, inline]

abbrev MPSolutionGroup : Type

The generic solution group of the Mermin-Peres magic square system.

Equations

• MPSolutionGroup = SolutionGroup magic_square_system

def MagicSquareSolutionGroup.linearSystem : LinearSystem

The magic square linear system, recovered from the support layout and game.

Equations

• MagicSquareSolutionGroup.linearSystem = magic_square_system

@[reducible, inline]

abbrev MagicSquareSolutionGroup.solutionGroup : Type

The solution group of the magic square linear system.

Equations

• MagicSquareSolutionGroup.solutionGroup = SolutionGroup MagicSquareSolutionGroup.linearSystem

def MagicSquareSolutionGroup.coefficientRow (i : Fin linearSystem.layout.r) : List ℕ

The coefficient row of equation i, rendered as a list of 0/1 naturals.

Equations

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

def MagicSquareSolutionGroup.coefficientMatrix : List (List ℕ)

The full coefficient matrix, rendered as rows of 0/1 naturals.

Equations

• MagicSquareSolutionGroup.coefficientMatrix = List.map MagicSquareSolutionGroup.coefficientRow (List.finRange MagicSquareSolutionGroup.linearSystem.layout.r)

def MagicSquareSolutionGroup.rhsVector : List ℕ

The right-hand side vector, rendered as a list of 0/1 naturals.

Equations

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

def MagicSquareSolutionGroup.equationSupportIndices (i : Fin linearSystem.layout.r) : List ℕ

The variables occurring in equation i, rendered as zero-based indices.

Equations

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

def MagicSquareSolutionGroup.equationSupports : List (List ℕ)

All equation supports, rendered as zero-based variable indices.

Equations

• MagicSquareSolutionGroup.equationSupports = List.map MagicSquareSolutionGroup.equationSupportIndices (List.finRange MagicSquareSolutionGroup.linearSystem.layout.r)

def MagicSquareSolutionGroup.equationPresentation : List (List ℕ × ℕ)

The equation relators in presentation form: ([variables in the equation], parity), where parity 1 means the product is J.

Equations

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

def MagicSquareSolutionGroup.formattedRelators : List String

The full solution-group relator list rendered with one-indexed generators.

Equations

• MagicSquareSolutionGroup.formattedRelators = List.map formatRelator (solutionRelatorsList magic_square_system)