3. Formalising Linear Constraint System Games🔗

To even start proving anything about LCS games, we first need to formalise what an LCS game is and what is a valid strategy for a game. This involves defining the geometry of the game, the requirements for a strategy to be valid, and the specific values of the constraints that define the game.

All of the content below is defined in the module LCS.Basic.

3.1. Defining the Layout of an LCS Game 🔗

A LCS Game is defined by his sets of variables and constraints.

We choose to represent the geometry of the game using a structure called LCSLayout, which contains the following data:

r : the number of constraints (or questions for Alice)
s : the number of variables (or questions for Bob)
V : a function that takes an index i and returns the set of variables that are involved in the i-th constraint.

structure LCSLayout where
  r : ℕ
  s : ℕ
  V : Fin r → Finset (Fin s)

Note that this layout does not contain any information about the specific values of the constraints, it only captures the geometry of the game, i.e. which variables are involved in which constraints. The specific values of the constraints will be captured in the definition of the LCS Game itself. This follows from the fact that a strategy for the game does not depend on the specific values of theconstraints, but only on the geometry of the game.

3.2. Assignments🔗

Assignemnt is an abreviation/aliases for the type, (function type) that represents all possible assignments of values to the variables in V i.

An assignement is defined for a specific LCS layout and a specific constraint i. The assignment of the variable to the constraint i is represented as a function that takes a variable from V_i and returns a value in Fin 2 (i.e. 0 or 1). This captures the idea that Alice must assign a value of 0 or 1 to each variable used in the i-th constraint.

Leans know that this is a function type that has a finite domain which will allow us for example to sum over all possible assignments in a finite way, which is important for the rest of the formalisation.

abbrev Assignment (G : LCSLayout) (i : Fin G.r) : Type :=
  (G.V i) → Fin 2

3.3. A LCS Game🔗

So far we have defined the geometry of the game, and the requirement for a strategy to be valid without ever specifying the specific values of the constraints. However as we will need to talk about winning assignements or winning strategies, we need to define the values of the contraints.

A LCS game is defined for a layout G. It is represent as a function that takes an index i to a value in ZMod 2 (i.e. 0 or 1). This captures the idea that the i-th constraint requires that the sum of the variables involved in that constraint must be equal to 0 or 1

structure LCSGame (G : LCSLayout) where
  b : Fin G.r → ZMod 2

3.4. A Valid Strategy for an LCS Game🔗

A strategy for an LCS game is modeled by a family of projectors for Alice and a family of projectors for Bob, that satisfy certain conditions. Specifically, the projectors for Alice must form a measurement system for each constraint, and the projectors for Bob must be consistent with the projectors for Alice in a certain way. This is captured by the definition of a valid strategy for an LCS game.

structure LCSStrategy
  (R : Type*) [Ring R] [StarRing R] [Algebra ℂ R]
  (G : LCSLayout) where
  E : ∀ i, (Assignment G i → R)
  F : Fin G.s → (Fin 2 → R)
  alice_ms : ∀ i, IsMeasurementSystem (E i)
  bob_ms   : ∀ j, IsMeasurementSystem (F j)
  commute  : ∀ i j α β, E i α * F j β = F j β * E i α

3.4.1. Measurement Systems🔗

The mathematical structure that captures the idea of a quantum measurement in the context of our LCS game.

structure IsMeasurementSystem
  {I : Type*} [Fintype I]
  (f : I → R) : Prop where
  sum_one      : ∑ x, f x = 1
  idempotent   : ∀ x, f x * f x = f x
  orthogonal   : ∀ x y, x ≠ y → f x * f y = 0
  self_adjoint : ∀ x, star (f x) = f x

3.5. Alice and Bob's Observables🔗

Given a strategy for an LCS game, we can define the observables for Alice and Bob. The observable for Alice corresponding to the variable j in the constraint i is defined as the difference between the sum of the projectors corresponding to the assignments that assign 0 to j and the sum of the projectors corresponding to the assignments that assign 1 to j.

For Bob, the observable corresponding to the variable j is defined as the difference between the projectors corresponding to the assignment that assigns 0 to j and the projectors corresponding to the assignment that assigns 1 to j.

Alice and Bob's observables are completly defined by the LCSstrategy object, which contains the projectors for Alice and Bob.

3.5.1. Alice's observable🔗

noncomputable def Alice_A
  {G : LCSLayout}
  {R : Type*} [Ring R] [StarRing R] [Algebra ℂ R]
  (strat : LCSStrategy R G) (i : Fin G.r) (j : G.V i) : R :=
  (∑ x ∈ Finset.univ.filter (fun (x : Assignment G i) => x j = 0), strat.E i x) -
  (∑ x ∈ Finset.univ.filter (fun (x : Assignment G i) => x j = 1), strat.E i x)

3.5.2. Bob's observable🔗

def Bob_B
  {R : Type*} [Ring R] [StarRing R] [Algebra ℂ R]
  {G : LCSLayout}
  (strat : LCSStrategy R G) (j : Fin G.s) : R :=
  strat.F j 0 - strat.F j 1