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

• ProjectorStrategy: The core structure representing a projector-based strategy.
• ProjectorStrategy.aliceObs, ProjectorStrategy.bobObs: Derived observables extracted from the projector measurements.

Key Lemmas

• ProjectorStrategy.isObservable_aliceObs, ProjectorStrategy.isObservable_bobObs: Proves that the derived operators are observables.
• ProjectorStrategy.aliceObs_commute, alice_bob_commute: Verification of commutation relations.

structure MIPRE.LCS.ProjectorStrategy (R : Type u_2) [Ring R] [StarRing R] (G : Layout) : Type u_2

A projector-based strategy for the LCS layout G: Alice has one measurement per equation, with outcomes the local assignments; Bob has one binary measurement per variable; and every projector of Alice commutes with every projector of Bob.

• E (i : Fin G.r) : G.Assignment i → R

  Alice's measurement for equation i, indexed by local assignments.

• F : Fin G.s → ZMod 2 → R

  Bob's binary measurement for each variable.

• alice_ms (i : Fin G.r) : IsMeasurementSystem (self.E i)

  Alice's families are measurement systems.

• bob_ms (j : Fin G.s) : IsMeasurementSystem (self.F j)

  Bob's families are measurement systems.

• alice_bob_commute (i : Fin G.r) (j : Fin G.s) (α : G.Assignment i) (β : ZMod 2) : self.E i α * self.F j β = self.F j β * self.E i α

  Every projector of Alice commutes with every projector of Bob.

noncomputable def MIPRE.LCS.ProjectorStrategy.aliceObs {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : R

Alice's derived observable for variable j in equation i: the ±1-observable of the marginal of her equation-i measurement on the j-th coordinate.

Equations

• strat.aliceObs i j = MIPRE.LCS.observableOfMeasurementSystem (MIPRE.LCS.inducedMeasurementSystem (strat.E i) fun (x : G.Assignment i) => x j)

def MIPRE.LCS.ProjectorStrategy.bobObs {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (j : Fin G.s) : R

Bob's derived observable F j 0 - F j 1 for variable j.

Equations

• strat.bobObs j = MIPRE.LCS.observableOfMeasurementSystem (strat.F j)

theorem MIPRE.LCS.ProjectorStrategy.isObservable_bobObs {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (j : Fin G.s) : IsObservable (strat.bobObs j)

theorem MIPRE.LCS.ProjectorStrategy.isObservable_aliceObs {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : IsObservable (strat.aliceObs i j)

theorem MIPRE.LCS.ProjectorStrategy.aliceObs_commute {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (j j' : ↥(G.V i)) : Commute (strat.aliceObs i j) (strat.aliceObs i j')

theorem MIPRE.LCS.ProjectorStrategy.aliceObs_commute_bobObs {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (k : ↥(G.V i)) (j_var : Fin G.s) : Commute (strat.aliceObs i k) (strat.bobObs j_var)

theorem MIPRE.LCS.ProjectorStrategy.aliceObs_mul_E {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) (x : G.Assignment i) : strat.aliceObs i j * strat.E i x = (-1) ^ (x j).val • strat.E i x

theorem MIPRE.LCS.ProjectorStrategy.aliceObs_noncommProd_mul_E {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (x : G.Assignment i) (comm : (↑s).Pairwise fun (j j' : ↥(G.V i)) => Commute (strat.aliceObs i j) (strat.aliceObs i j')) : s.noncommProd (fun (j : ↥(G.V i)) => strat.aliceObs i j) comm * strat.E i x = (∏ j ∈ s, (-1) ^ (x j).val) • strat.E i x

noncomputable def MIPRE.LCS.ProjectorStrategy.aliceRowProd {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) : R

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

Equations

• strat.aliceRowProd i = (G.V i).attach.noncommProd (fun (j : ↥(G.V i)) => strat.aliceObs i j) ⋯

theorem MIPRE.LCS.ProjectorStrategy.bobObs_commute_aliceRowProd {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : Commute (strat.bobObs ↑j) (strat.aliceRowProd i)

theorem MIPRE.LCS.ProjectorStrategy.aliceObs_commute_aliceRowProd {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : Commute (strat.aliceObs i j) (strat.aliceRowProd i)

theorem MIPRE.LCS.ProjectorStrategy.bob_measurement_recover {R : Type u_1} [Ring R] [StarRing R] {G : Layout} (strat : ProjectorStrategy R G) (j : Fin G.s) : strat.F j 0 - strat.F j 1 = strat.bobObs j ∧ strat.F j 0 + strat.F j 1 = 1

theorem MIPRE.LCS.ProjectorStrategy.F_eq_observableToProjector {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (strat : ProjectorStrategy R G) (j : Fin G.s) (y : ZMod 2) : strat.F j y = observableToProjector (strat.bobObs j) y