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_To_ProjectorStrategy, which converts an ObservableStrategyData into an LCSStrategy. 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 BobMeasurementFromObservables {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) : Fin G.s → Fin 2 → R

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

Equations

• BobMeasurementFromObservables S j y = ObservableToProjector (S.bob_obs j) y

theorem bobMeasurementFromObservables_isMeasurementSystem {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (j : Fin G.s) : IsMeasurementSystem (BobMeasurementFromObservables S j)

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

theorem projector_commute_in_equation {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) (j k : ↥(G.V i)) (a b : Fin 2) : Commute (ObservableToProjector (S.alice_obs ↑j) a) (ObservableToProjector (S.alice_obs ↑k) b)

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

noncomputable def AliceMeasurementFromObservables {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) : Assignment G 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

• AliceMeasurementFromObservables S i assignment = Finset.univ.noncommProd (fun (j_idx : ↥(G.V i)) => ObservableToProjector (S.alice_obs ↑j_idx) (assignment j_idx)) ⋯

noncomputable def JointOn {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) (s : Finset ↥(G.V i)) (assignment : (j : ↥(G.V i)) → j ∈ s → Fin 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

• JointOn S i s assignment = s.noncommProd (fun (j : ↥(G.V i)) => if hj : j ∈ s then ObservableToProjector (S.alice_obs ↑j) (assignment j hj) else 1) ⋯

theorem jointOn_sum_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) : ∑ assignment : (j : ↥(G.V i)) → j ∈ Finset.univ → Fin 2, JointOn S i Finset.univ assignment = 1

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

theorem aliceMeasurementFromObservables_sum_one {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) : ∑ assignment : Assignment G i, AliceMeasurementFromObservables S i assignment = 1

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

theorem aliceMeasurementFromObservables_isMeasurementSystem {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) : IsMeasurementSystem (AliceMeasurementFromObservables S i)

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

theorem aliceMeasurement_bobMeasurement_commute {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) (j : Fin G.s) (α : Assignment G i) (β : Fin 2) : AliceMeasurementFromObservables S i α * BobMeasurementFromObservables S j β = BobMeasurementFromObservables S j β * AliceMeasurementFromObservables S 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 aliceObservable_mul_aliceMeasurementFromObservables {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) (j : ↥(G.V i)) (assignment : Assignment G i) : S.alice_obs ↑j * AliceMeasurementFromObservables S i assignment = (-1) ^ ↑(assignment j) • AliceMeasurementFromObservables S i assignment

noncomputable def ObservableStrategy_To_ProjectorStrategy {R : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) : LCSStrategy R G

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

Equations

• ObservableStrategy_To_ProjectorStrategy S = { E := AliceMeasurementFromObservables S, F := BobMeasurementFromObservables S, alice_ms := ⋯, bob_ms := ⋯, commute := ⋯ }

theorem alice_A_observableStrategy {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (i : Fin G.r) (j : ↥(G.V i)) : Alice_A (ObservableStrategy_To_ProjectorStrategy S) i j = S.alice_obs ↑j

theorem bob_B_observableStrategy {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] {G : LCSLayout} (S : ObservableStrategyData R G) (j : Fin G.s) : Bob_B (ObservableStrategy_To_ProjectorStrategy S) j = S.bob_obs j

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