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, together with helpers rendering the presentation data (coefficient matrix, right-hand side, and equation supports) as plain lists.

def MIPRE.LCS.MagicSquare.linearSystem : LinearSystem

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

Equations

• MIPRE.LCS.MagicSquare.linearSystem = MIPRE.LCS.MagicSquare.game.toLinearSystem

@[reducible, inline]

abbrev MIPRE.LCS.MagicSquare.solutionGroup : Type

The solution group of the magic square linear system.

Equations

• MIPRE.LCS.MagicSquare.solutionGroup = MIPRE.LCS.SolutionGroup MIPRE.LCS.MagicSquare.linearSystem

def MIPRE.LCS.MagicSquare.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 MIPRE.LCS.MagicSquare.coefficientMatrix : List (List ℕ)

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

Equations

• MIPRE.LCS.MagicSquare.coefficientMatrix = List.map MIPRE.LCS.MagicSquare.coefficientRow (List.finRange MIPRE.LCS.MagicSquare.linearSystem.layout.r)

def MIPRE.LCS.MagicSquare.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 MIPRE.LCS.MagicSquare.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 MIPRE.LCS.MagicSquare.equationSupports : List (List ℕ)

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

Equations

• MIPRE.LCS.MagicSquare.equationSupports = List.map MIPRE.LCS.MagicSquare.equationSupportIndices (List.finRange MIPRE.LCS.MagicSquare.linearSystem.layout.r)

def MIPRE.LCS.MagicSquare.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.