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

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

structure LCSLayout : Type

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

@[reducible, inline]

abbrev Assignment (G : LCSLayout) (i : Fin G.r) : Type

Equations

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

structure LCSGame (G : LCSLayout) : Type

• b : Fin G.r → Fin 2

structure LinearSystem : Type

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

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

def LCSGame.toLinearSystem {G : LCSLayout} (game : LCSGame 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 }