Equivalence between Observable-based and Projector-based Strategies

This module establishes the equivalence between the two main formalisms for LCS strategies:

1. Observable-based strategies: Defined in terms of self-adjoint involutive operators $A_j, B_k$ satisfying local commutation constraints.
2. Projector-based strategies: Defined in terms of projector measurement systems $E_{i,x}, F_{j,y}$ satisfying similar commutation and consistency constraints.

The main construction in this file is ObservableStrategy.toProjectorStrategy, which converts an ObservableStrategy into an ProjectorStrategy. It proves that:

• The induced Alice measurements $E_{i,x}$ (defined as products of projectors) and Bob measurements $F_{j,y}$ (derived from Bob's observables) form valid measurement systems.
• Alice and Bob's measurements commute as required by the LCS game structure.

noncomputable def MIPRE.LCS.ObservableStrategy.bobMeasurement {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) : Fin G.s → ZMod 2 → R

Bob's two-outcome measurement obtained from his observable via $P_y = (1/2)(1 + (-1)^y B_j)$.

Equations

• S.bobMeasurement j y = MIPRE.LCS.observableToProjector (S.bobObs j) y

theorem MIPRE.LCS.ObservableStrategy.isMeasurementSystem_bobMeasurement {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : Layout} (S : ObservableStrategy R G) (j : Fin G.s) : IsMeasurementSystem (S.bobMeasurement j)

For each question $j$, Bob's observable-induced projectors form a measurement system.

theorem MIPRE.LCS.ObservableStrategy.projector_commute_in_equation {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (j k : ↥(G.V i)) (a b : ZMod 2) : Commute (observableToProjector (S.aliceObs ↑j) a) (observableToProjector (S.aliceObs ↑k) b)

Projectors built from Alice observables belonging to the same equation commute, because the underlying observables commute.

noncomputable def MIPRE.LCS.ObservableStrategy.aliceMeasurement {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) : G.Assignment i → R

Alice's projector for an assignment $x$ is the product $E_{i,x} = \prod_{j \in V_i} (1/2)(1 + (-1)^{x_j} A_j)$.

Equations

• S.aliceMeasurement i assignment = Finset.univ.noncommProd (fun (j_idx : ↥(G.V i)) => MIPRE.LCS.observableToProjector (S.aliceObs ↑j_idx) (assignment j_idx)) ⋯

noncomputable def MIPRE.LCS.ObservableStrategy.jointOn {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (assignment : (j : ↥(G.V i)) → j ∈ s → ZMod 2) : R

Partial joint measurement over a finite subset $s \subseteq V_i$. This is used to prove the normalization of Alice's full measurement by induction on $s$.

Equations

• S.jointOn i s assignment = s.noncommProd (fun (j : ↥(G.V i)) => if hj : j ∈ s then MIPRE.LCS.observableToProjector (S.aliceObs ↑j) (assignment j hj) else 1) ⋯

theorem MIPRE.LCS.ObservableStrategy.jointOn_sum_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) : ∑ assignment : (j : ↥(G.V i)) → j ∈ Finset.univ → ZMod 2, S.jointOn i Finset.univ assignment = 1

Summing the partial joint projectors over all assignments on $s = V_i$ gives $1$.

theorem MIPRE.LCS.ObservableStrategy.aliceMeasurement_sum_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) : ∑ assignment : G.Assignment i, S.aliceMeasurement i assignment = 1

Alice's full assignment-indexed projectors sum to $1$.

theorem MIPRE.LCS.projector_orthogonal_of_ne {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (O : R) (hO : IsObservable O) (a b : ZMod 2) (hab : a ≠ b) : observableToProjector O a * observableToProjector O b = 0

Two distinct outcomes for the projector associated to a single observable are orthogonal.

theorem MIPRE.LCS.alice_partial_idempotent {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (assignment : G.Assignment i) : let f := fun (j : ↥(G.V i)) => observableToProjector (S.aliceObs ↑j) (assignment j); s.noncommProd f ⋯ * s.noncommProd f ⋯ = s.noncommProd f ⋯

The partial Alice measurement over $s$ is idempotent.

theorem MIPRE.LCS.alice_partial_selfAdjoint {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (assignment : G.Assignment i) : let f := fun (j : ↥(G.V i)) => observableToProjector (S.aliceObs ↑j) (assignment j); star (s.noncommProd f ⋯) = s.noncommProd f ⋯

The partial Alice measurement over $s$ is self-adjoint.

theorem MIPRE.LCS.alice_partial_orthogonal {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (α β : G.Assignment i) (j0 : ↥(G.V i)) (hj0 : j0 ∈ s) (hneq : α j0 ≠ β j0) : let fα := fun (j : ↥(G.V i)) => observableToProjector (S.aliceObs ↑j) (α j); let fβ := fun (j : ↥(G.V i)) => observableToProjector (S.aliceObs ↑j) (β j); s.noncommProd fα ⋯ * s.noncommProd fβ ⋯ = 0

If two assignments differ at some $j₀ \in s$, then the corresponding partial Alice projectors are orthogonal.

theorem MIPRE.LCS.ObservableStrategy.isMeasurementSystem_aliceMeasurement {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) : IsMeasurementSystem (S.aliceMeasurement i)

For each equation $i$, the assignment-indexed family of Alice projectors is a measurement system.

theorem MIPRE.LCS.ObservableStrategy.aliceMeasurement_commute_bobMeasurement {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (j : Fin G.s) (α : G.Assignment i) (β : ZMod 2) : S.aliceMeasurement i α * S.bobMeasurement j β = S.bobMeasurement j β * S.aliceMeasurement i α

Every Alice projector commutes with every Bob projector, because each Alice observable commutes with each Bob observable and commutation is preserved by the projector construction.

theorem MIPRE.LCS.ObservableStrategy.aliceObs_mul_aliceMeasurement {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) (assignment : G.Assignment i) : S.aliceObs ↑j * S.aliceMeasurement i assignment = (-1) ^ (assignment j).val • S.aliceMeasurement i assignment

noncomputable def MIPRE.LCS.ObservableStrategy.toProjectorStrategy {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : Layout} (S : ObservableStrategy R G) : ProjectorStrategy R G

The observable strategy data induces a projector-valued LCS strategy by taking, for each observable, its associated two-outcome spectral projectors.

Equations

• S.toProjectorStrategy = { E := S.aliceMeasurement, F := S.bobMeasurement, alice_ms := ⋯, bob_ms := ⋯, alice_bob_commute := ⋯ }

theorem MIPRE.LCS.ObservableStrategy.toProjectorStrategy_aliceObs {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : Layout} (S : ObservableStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : S.toProjectorStrategy.aliceObs i j = S.aliceObs ↑j

theorem MIPRE.LCS.ObservableStrategy.toProjectorStrategy_bobObs {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : Layout} (S : ObservableStrategy R G) (j : Fin G.s) : S.toProjectorStrategy.bobObs j = S.bobObs j

The Bob observable recovered from the projector strategy is the original observable supplied to the observable strategy.

noncomputable def MIPRE.LCS.BipartiteObservableStrategy.toProjectorStrategy {n : Type u_2} [Fintype n] [DecidableEq n] {G : Layout} (strat : BipartiteObservableStrategy n G) : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G

The projector strategy induced by a bipartite observable strategy through toObservableStrategy.

Equations

• strat.toProjectorStrategy = strat.toObservableStrategy.toProjectorStrategy

@[simp]

theorem MIPRE.LCS.BipartiteObservableStrategy.toProjectorStrategy_aliceObs {n : Type u_2} [Fintype n] [DecidableEq n] {G : Layout} (strat : BipartiteObservableStrategy n G) (i : Fin G.r) (j : ↥(G.V i)) : strat.toProjectorStrategy.aliceObs i j = bipartiteAliceLift (strat.obs ↑j)

@[simp]

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