Linear Constraint System (LCS) Game Layout

This module defines the basic geometric structure of a Linear Constraint System (LCS) game. An LCS game is defined by a set of binary variables and a set of linear equations over $\mathbb{F}_2$.

Key Definitions

• Layout: The structure describing the relationship between equations and variables.
• Layout.Assignment: A local mapping of values to variables in a specific equation.
• Game: The specification of the right-hand sides of the linear equations.

structure MIPRE.LCS.Layout : Type

The layout of a binary linear constraint system: r equations over s variables, with V i the set of variables occurring in equation i.

• r : ℕ

  The number of equations.

• s : ℕ

  The number of variables.

• V : Fin self.r → Finset (Fin self.s)

  The support of each equation: V i is the set of variables occurring in equation i.

@[reducible, inline]

abbrev MIPRE.LCS.Layout.Assignment (G : Layout) (i : Fin G.r) : Type

A local assignment of 𝔽₂-values to the variables of equation i.

Equations

• G.Assignment i = (↥(G.V i) → ZMod 2)

structure MIPRE.LCS.Game (G : Layout) : Type

An LCS game over the layout G, given by the right-hand sides of the equations.

• b : Fin G.r → ZMod 2

  The right-hand side of each equation.

structure MIPRE.LCS.LinearSystem : Type

A full binary linear system with explicit coefficient matrix and right-hand side.

• layout : Layout
• A : Fin self.layout.r → Fin self.layout.s → ZMod 2
• b : Fin self.layout.r → ZMod 2

def MIPRE.LCS.Game.toLinearSystem {G : Layout} (game : Game G) : LinearSystem

Recover the explicit binary linear system encoded by a support-only LCS game.

Equations

• game.toLinearSystem = { layout := G, A := fun (i : Fin G.r) (j : Fin G.s) => if j ∈ G.V i then 1 else 0, b := game.b }