Linear Constraint System Games in Lean

This project formalizes Linear Constraint System (LCS) games in Lean 4, with a focus on quantum strategies, the Mermin-Peres magic square example, and the operator-theoretic conditions behind perfect play.

The formal development has two main goals: relate the observable description of a strategy to the projector-based one, and prove winning conditions through the analysis of the local loss operator.

The library is organized around core game definitions, algebraic foundations for observables and measurements, strategy constructions, and theorem files proving the main results.

Browse the GitHub repository for the source, or read the manual at lcs.perazzolo.ch for a guided presentation.