Observable-based Strategy for LCS Games

This module defines the data structure for a strategy in a Linear Constraint System (LCS) game using the observable formalism. In this formalism, players choose observables (self-adjoint involutive operators) instead of projectors.

Key Definitions

• ObservableStrategy: The data representing an observable strategy, including:
  • aliceObs, bobObs: The observables for Alice and Bob.
  • sameEquation_comm: The local commutativity of Alice's observables within an equation.
  • alice_bob_commute: The global commutativity between Alice's and Bob's observables.

structure MIPRE.LCS.ObservableStrategy (R : Type u_1) [Ring R] [StarRing R] (G : Layout) : Type u_1

An observable-based strategy for the LCS layout G: Alice and Bob each assign a binary observable to every variable, Alice's observables commute within each equation, and every observable of Alice commutes with every observable of Bob.

• aliceObs : Fin G.s → R

  Alice's observable for each variable.

• bobObs : Fin G.s → R

  Bob's observable for each variable.

• alice_isObservable (j : Fin G.s) : IsObservable (self.aliceObs j)

  Alice's operators are observables.

• bob_isObservable (j : Fin G.s) : IsObservable (self.bobObs j)

  Bob's operators are observables.

• sameEquation_comm (i : Fin G.r) : Pairwise fun (j k : ↥(G.V i)) => Commute (self.aliceObs ↑j) (self.aliceObs ↑k)

  Alice's observables commute within each equation.

• alice_bob_commute (j k : Fin G.s) : Commute (self.aliceObs j) (self.bobObs k)

  Every observable of Alice commutes with every observable of Bob.

def MIPRE.LCS.bipartiteAliceLift {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℂ) : Matrix (n × n) (n × n) ℂ

Alice's side of the bipartite lift, M ↦ M ⊗ 1.

Equations

• MIPRE.LCS.bipartiteAliceLift M = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1

def MIPRE.LCS.bipartiteBobLift {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℂ) : Matrix (n × n) (n × n) ℂ

Bob's side of the bipartite lift, M ↦ 1 ⊗ M.

Equations

• MIPRE.LCS.bipartiteBobLift M = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M

theorem MIPRE.LCS.isObservable_bipartiteAliceLift {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (h : IsObservable M) : IsObservable (bipartiteAliceLift M)

theorem MIPRE.LCS.isObservable_bipartiteBobLift {n : Type u_1} [Fintype n] [DecidableEq n] {M : Matrix n n ℂ} (h : IsObservable M) : IsObservable (bipartiteBobLift M)

theorem MIPRE.LCS.bipartiteAliceLift_commute_bipartiteBobLift {n : Type u_1} [Fintype n] [DecidableEq n] (M N : Matrix n n ℂ) : Commute (bipartiteAliceLift M) (bipartiteBobLift N)

theorem MIPRE.LCS.bipartiteAliceLift_commute {n : Type u_1} [Fintype n] [DecidableEq n] {M N : Matrix n n ℂ} (h : Commute M N) : Commute (bipartiteAliceLift M) (bipartiteAliceLift N)

structure MIPRE.LCS.BipartiteObservableStrategy (n : Type u_1) [Fintype n] [DecidableEq n] (G : Layout) : Type u_1

A bipartite observable strategy: a single grid of observables on ℂ^n, commuting within each equation, which both players use through the Kronecker lifts M ⊗ 1 and 1 ⊗ M (see toObservableStrategy).

• obs : Fin G.s → Matrix n n ℂ

  The grid of observables, one per variable.

• isObservable (j : Fin G.s) : IsObservable (self.obs j)

  Each grid entry is an observable.

• sameEquation_comm (i : Fin G.r) : Pairwise fun (j k : ↥(G.V i)) => Commute (self.obs ↑j) (self.obs ↑k)

  Grid observables commute within each equation.

noncomputable def MIPRE.LCS.BipartiteObservableStrategy.toObservableStrategy {n : Type u_1} [Fintype n] [DecidableEq n] {G : Layout} (strat : BipartiteObservableStrategy n G) : ObservableStrategy (Matrix (n × n) (n × n) ℂ) G

The observable strategy on ℂ^n ⊗ ℂ^n induced by a bipartite strategy: Alice plays M ⊗ 1 and Bob plays 1 ⊗ M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LCS.BipartiteObservableStrategy.toObservableStrategy_aliceObs {n : Type u_1} [Fintype n] [DecidableEq n] {G : Layout} (strat : BipartiteObservableStrategy n G) (j : Fin G.s) : strat.toObservableStrategy.aliceObs j = bipartiteAliceLift (strat.obs j)

@[simp]

theorem MIPRE.LCS.BipartiteObservableStrategy.toObservableStrategy_bobObs {n : Type u_1} [Fintype n] [DecidableEq n] {G : Layout} (strat : BipartiteObservableStrategy n G) (j : Fin G.s) : strat.toObservableStrategy.bobObs j = bipartiteBobLift (strat.obs j)