Projector-based Strategy for LCS Games

This module defines the standard formalism for LCS game strategies using projector measurement systems. In this formalism, players' strategies are represented by families of projectors $\{E_{i,x}\}$ and $\{F_{j,y}\}$.

Key Definitions

• LCSStrategy: The core structure representing a projector-based strategy.
• Alice_A, Bob_B: Derived observables extracted from the projector measurements.

Key Lemmas

• alice_is_observable, bob_is_observable: Proves that the derived operators are observables.
• alice_observables_commute, alice_bob_commute: Verification of commutation relations.

structure LCSStrategy (R : Type u_2) [Ring R] [StarRing R] [Algebra ℂ R] (G : LCSLayout) : Type u_2

• E (i : Fin G.r) : Assignment G i → R
• F : Fin G.s → Fin 2 → R
• alice_ms (i : Fin G.r) : IsMeasurementSystem (self.E i)
• bob_ms (j : Fin G.s) : IsMeasurementSystem (self.F j)
• commute (i : Fin G.r) (j : Fin G.s) (α : Assignment G i) (β : Fin 2) : self.E i α * self.F j β = self.F j β * self.E i α

noncomputable def Alice_A {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : R

Equations

• Alice_A strat i j = ObservableOfMeasurementSystem (InducedMeasurementSystem (strat.E i) fun (x : Assignment G i) => x j)

def Bob_B {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (j : Fin G.s) : R

Equations

• Bob_B strat j = ObservableOfMeasurementSystem (strat.F j)

theorem bob_is_observable {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (j : Fin G.s) : IsObservable (Bob_B strat j)

theorem alice_is_observable {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : IsObservable (Alice_A strat i j)

theorem alice_observables_commute {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (j j' : ↥(G.V i)) : Commute (Alice_A strat i j) (Alice_A strat i j')

theorem alice_bob_commute_gen {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (k : ↥(G.V i)) (j_var : Fin G.s) : Commute (Alice_A strat i k) (Bob_B strat j_var)

theorem alice_A_mul_projector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) (x : Assignment G i) : Alice_A strat i j * strat.E i x = (-1) ^ ↑(x j) • strat.E i x

theorem alice_partial_prod_mul_projector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (x : Assignment G i) (comm : (↑s).Pairwise fun (j j' : ↥(G.V i)) => Commute (Alice_A strat i j) (Alice_A strat i j')) : s.noncommProd (fun (j : ↥(G.V i)) => Alice_A strat i j) comm * strat.E i x = (∏ j ∈ s, (-1) ^ ↑(x j)) • strat.E i x

noncomputable def Alice_Row_Prod {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) : R

The product of Alice's observables for all variables in equation i.

Equations

• Alice_Row_Prod strat i = (G.V i).attach.noncommProd (fun (j : { x : Fin G.s // x ∈ G.V i }) => Alice_A strat i j) ⋯

theorem bob_commute_row_prod {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : Commute (Bob_B strat ↑j) (Alice_Row_Prod strat i)

theorem alice_commute_row_prod {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : Commute (Alice_A strat i j) (Alice_Row_Prod strat i)

theorem bob_measurement_recover {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (j : Fin G.s) : strat.F j 0 - strat.F j 1 = Bob_B strat j ∧ strat.F j 0 + strat.F j 1 = 1

theorem bob_measurement_eq_projector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (strat : LCSStrategy R G) (j : Fin G.s) (y : Fin 2) : strat.F j y = ObservableToProjector (Bob_B strat j) y