The nonlocal game of a linear constraint system

This file interprets an LCS instance (MIPRE.LCS.Game) as a two-player one-round nonlocal game in the sense of MIPRE.Game, connecting the operator-algebraic perfect-play formalism of MIPRE.LCS with the game-value framework of MIPRE.Foundations.Games.

The game is symmetric in the players

Both players receive questions from the same alphabet Fin G.r ⊕ Fin G.s --- an equation or a variable --- and answer in the same alphabet (Fin G.s → ZMod 2) ⊕ ZMod 2 --- an assignment or a bit. The referee samples an incidence (i, j) with j ∈ G.V i and then a uniform orientation: one player is asked the equation and the other the variable. So there are 2 r |V i|-many equiprobable oriented pairs, and both players have measurements at both kinds of question.

That is deliberate, and it is what the literature's game^MS means. An earlier version of this file sent the equation to Alice and the variable to Bob always. Nothing in the repository depended on that choice, and it made statements about both players' variable observables --- which is what the Pauli basis test consumes from the Magic Square, blueprint lem:ms-direct-anticomm --- inexpressible: Alice never received a variable question, so A^{Variable_j} did not exist. The orientation also fixes the constant of that lemma: the sum of the conditional failures over the oriented incidences is 2 r |V i| times the failure probability rather than r |V i| times it.

The decider checks the shape

Game.accepts rejects an answer whose shape does not match its question, and rejects an off-support pair (i, j) with j ∉ G.V i. Neither check is redundant with the question distribution vanishing there. reports/clgame-format-check-missing.md records what a missing format check cost the seeded CL game: the test became vacuous and a soundness theorem about it false. The accepts_* simp lemmas below and the decide-checked witnesses in MIPRE/LCS/MagicSquare/Game.lean --- an accepted pair in each orientation, and one rejected for each of the three reasons --- are the guard against a repeat.

Main definitions

• MIPRE.LCS.Layout.Question, MIPRE.LCS.Layout.Answer: the shared question and answer alphabets;
• MIPRE.LCS.Layout.questionDist: the oriented-incidence distribution;
• MIPRE.LCS.Game.accepts: the decider;
• MIPRE.LCS.Game.toNonlocalGame: the nonlocal game of an LCS instance.

Main statements

• MIPRE.LCS.exists_tensorStrategy_value_eq_one_of_localLoss_annihilates_epr: a bipartite observable strategy whose local loss operators annihilate the (unnormalized) EPR vector yields a perfect tensor-product strategy for the associated nonlocal game.

The alphabets

@[reducible, inline]

abbrev MIPRE.LCS.Layout.Question (G : Layout) : Type

A question of the LCS game: an equation (inl) or a variable (inr). Both players receive questions from this alphabet.

Equations

• G.Question = (Fin G.r ⊕ Fin G.s)

@[reducible, inline]

abbrev MIPRE.LCS.Layout.Answer (G : Layout) : Type

An answer: an assignment to all the variables (inl), which is what an equation question is answered with, or a single bit (inr), which is what a variable question is answered with. The decider rejects the shape that does not match the question, so the two are not interchangeable --- a player who answers a variable question with an assignment loses.

Equations

• G.Answer = ((Fin G.s → ZMod 2) ⊕ ZMod 2)

The question distribution

noncomputable def MIPRE.LCS.Layout.questionDist (G : Layout) : G.Question → G.Question → ℝ

The oriented-incidence distribution: an incidence (i, j) with j ∈ G.V i, then a uniform orientation. Each of the 2 ∑_i |V i| oriented pairs has probability 1 / (2 r |V i|).

Equations

• G.questionDist (Sum.inl i) (Sum.inr j) = if j ∈ G.V i then 1 / (2 * ↑G.r * ↑(G.V i).card) else 0
• G.questionDist (Sum.inr j) (Sum.inl i) = if j ∈ G.V i then 1 / (2 * ↑G.r * ↑(G.V i).card) else 0
• G.questionDist x✝¹ x✝ = 0

theorem MIPRE.LCS.Layout.questionDist_nonneg (G : Layout) (x y : G.Question) : 0 ≤ G.questionDist x y

theorem MIPRE.LCS.Layout.sum_questionDist_inl {G : Layout} (hr : 0 < G.r) (hV : ∀ (i : Fin G.r), (G.V i).Nonempty) (i : Fin G.r) : ∑ y : G.Question, G.questionDist (Sum.inl i) y = 1 / (2 * ↑G.r)

One player's row sums to 1 / (2 r) at an equation question: the variable is uniform in the equation's support and the orientation costs the factor two.

theorem MIPRE.LCS.Layout.sum_questionDist {G : Layout} (hr : 0 < G.r) (hV : ∀ (i : Fin G.r), (G.V i).Nonempty) : ∑ x : G.Question, ∑ y : G.Question, G.questionDist x y = 1

The decider

def MIPRE.LCS.Game.accepts {G : Layout} (game : Game G) : G.Question → G.Question → G.Answer → G.Answer → Bool

The decider: the answer shapes must match the questions, the incidence must be on support, the assignment must satisfy its equation, and it must agree with the other player's bit at his variable. Every other combination is rejected.

Equations

• game.accepts (Sum.inl i) (Sum.inr j) (Sum.inl a) (Sum.inr v) = (decide (j ∈ G.V i) && decide (∑ k ∈ G.V i, a k = game.b i) && decide (a j = v))
• game.accepts (Sum.inr j) (Sum.inl i) (Sum.inr v) (Sum.inl a) = (decide (j ∈ G.V i) && decide (∑ k ∈ G.V i, a k = game.b i) && decide (a j = v))
• game.accepts x✝³ x✝² x✝¹ x✝ = false

@[simp]

theorem MIPRE.LCS.Game.accepts_inl_inr_of_inr {G : Layout} (game : Game G) (i : Fin G.r) (j : Fin G.s) (v : ZMod 2) (c : G.Answer) : game.accepts (Sum.inl i) (Sum.inr j) (Sum.inr v) c = false

The decider rejects a mismatched shape. Answering an equation question with a bit, or a variable question with an assignment, loses --- whatever the other player does.

@[simp]

theorem MIPRE.LCS.Game.accepts_inl_inr_of_inl {G : Layout} (game : Game G) (i : Fin G.r) (j : Fin G.s) (a b : Fin G.s → ZMod 2) : game.accepts (Sum.inl i) (Sum.inr j) (Sum.inl a) (Sum.inl b) = false

@[simp]

theorem MIPRE.LCS.Game.accepts_same_kind_left {G : Layout} (game : Game G) (i i' : Fin G.r) (c d : G.Answer) : game.accepts (Sum.inl i) (Sum.inl i') c d = false

@[simp]

theorem MIPRE.LCS.Game.accepts_same_kind_right {G : Layout} (game : Game G) (j j' : Fin G.s) (c d : G.Answer) : game.accepts (Sum.inr j) (Sum.inr j') c d = false

theorem MIPRE.LCS.Game.accepts_eq_false_of_not_mem {G : Layout} (game : Game G) {i : Fin G.r} {j : Fin G.s} (h : j ∉ G.V i) (a : Fin G.s → ZMod 2) (v : ZMod 2) : game.accepts (Sum.inl i) (Sum.inr j) (Sum.inl a) (Sum.inr v) = false

The decider rejects an off-support incidence, independently of the question distribution vanishing there.

The symmetry between the players

The orientation is sampled uniformly and the decider reads the two sides symmetrically, so exchanging the players is an automorphism of the game. This is what lets a one-sided soundness statement be applied twice --- as blueprint lem:ms-direct-anticomm does, whose Alice half is its Bob half for the swapped strategy.

theorem MIPRE.LCS.Layout.questionDist_symm (G : Layout) (x y : G.Question) : G.questionDist x y = G.questionDist y x

theorem MIPRE.LCS.Game.accepts_symm {G : Layout} (game : Game G) (x y : G.Question) (c d : G.Answer) : game.accepts x y c d = game.accepts y x d c

The game

noncomputable def MIPRE.LCS.Game.toNonlocalGame {G : Layout} (game : Game G) (hr : 0 < G.r) (hV : ∀ (i : Fin G.r), (G.V i).Nonempty) : MIPRE.Game G.Question G.Question G.Answer G.Answer

The nonlocal game of an LCS instance. The referee samples an incidence (i, j) with j ∈ G.V i and a uniform orientation; the player who receives the equation answers an assignment (only its restriction to G.V i is read), the player who receives the variable answers a bit, and they win if the assignment satisfies the equation and agrees with the bit. The hypotheses hr and hV are what make questionDist a probability distribution.

Blueprint def:lcs-game.

Equations

• game.toNonlocalGame hr hV = { μ := G.questionDist, μ_nonneg := ⋯, μ_sum_one := ⋯, D := game.accepts }

@[simp]

theorem MIPRE.LCS.Game.toNonlocalGame_μ {G : Layout} (game : Game G) (hr : 0 < G.r) (hV : ∀ (i : Fin G.r), (G.V i).Nonempty) (x y : G.Question) : (game.toNonlocalGame hr hV).μ x y = G.questionDist x y

@[simp]

theorem MIPRE.LCS.Game.toNonlocalGame_D {G : Layout} (game : Game G) (hr : 0 < G.r) (hV : ∀ (i : Fin G.r), (G.V i).Nonempty) (x y : G.Question) (c d : G.Answer) : (game.toNonlocalGame hr hV).D x y c d = game.accepts x y c d

Perfect strategies from operator solutions

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

The local strategy on ℂ^n: Alice's observables are the grid, Bob's are trivial. Only its Alice measurement is used.

Equations

• strat.localStrategy = { aliceObs := strat.obs, bobObs := fun (x : Fin G.s) => 1, alice_isObservable := ⋯, bob_isObservable := ⋯, sameEquation_comm := ⋯, alice_bob_commute := ⋯ }

noncomputable def MIPRE.LCS.BipartiteObservableStrategy.aliceLiftHom {n : Type u_1} [Fintype n] [DecidableEq n] : Matrix n n ℂ →* Matrix (n × n) (n × n) ℂ

Alice's lift as a monoid homomorphism.

Equations

• MIPRE.LCS.BipartiteObservableStrategy.aliceLiftHom = { toFun := MIPRE.LCS.bipartiteAliceLift, map_one' := ⋯, map_mul' := ⋯ }

theorem MIPRE.LCS.BipartiteObservableStrategy.bipartiteAliceLift_observableToProjector {n : Type u_1} [Fintype n] [DecidableEq n] (O : Matrix n n ℂ) (a : ZMod 2) : bipartiteAliceLift (observableToProjector O a) = observableToProjector (bipartiteAliceLift O) a

theorem MIPRE.LCS.BipartiteObservableStrategy.bipartiteBobLift_observableToProjector {n : Type u_1} [Fintype n] [DecidableEq n] (O : Matrix n n ℂ) (a : ZMod 2) : bipartiteBobLift (observableToProjector O a) = observableToProjector (bipartiteBobLift O) a

theorem MIPRE.LCS.BipartiteObservableStrategy.toProjectorStrategy_E {G : Layout} {n : Type u_1} [Fintype n] [DecidableEq n] (strat : BipartiteObservableStrategy n G) (i : Fin G.r) (α : G.Assignment i) : strat.toProjectorStrategy.E i α = bipartiteAliceLift (strat.localStrategy.aliceMeasurement i α)

theorem MIPRE.LCS.BipartiteObservableStrategy.toProjectorStrategy_F {G : Layout} {n : Type u_1} [Fintype n] [DecidableEq n] (strat : BipartiteObservableStrategy n G) (j : Fin G.s) (v : ZMod 2) : strat.toProjectorStrategy.F j v = bipartiteBobLift (observableToProjector (strat.obs j) v)

Kronecker products of sums

theorem MIPRE.LCS.finset_sum_kronecker {ι : Type u_2} {m : Type u_3} [Fintype m] (s : Finset ι) (A : ι → Matrix m m ℂ) (B : Matrix m m ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (∑ i ∈ s, A i) B = ∑ i ∈ s, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (A i) B

theorem MIPRE.LCS.kronecker_finset_sum {ι : Type u_2} {m : Type u_3} [Fintype m] (s : Finset ι) (A : Matrix m m ℂ) (B : ι → Matrix m m ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A (∑ i ∈ s, B i) = ∑ i ∈ s, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A (B i)

theorem MIPRE.LCS.sum_induced_kron {I : Type u_2} {J : Type u_3} {I' : Type u_4} {J' : Type u_5} {m : Type u_6} [Fintype I] [Fintype J] [Fintype I'] [Fintype J'] [DecidableEq J] [DecidableEq J'] [Fintype m] [DecidableEq m] (E : I → Matrix m m ℂ) (F : I' → Matrix m m ℂ) (f : I → J) (g : I' → J') (c : J → J' → ℂ) : ∑ a : J, ∑ b : J', c a b • Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (inducedMeasurementSystem E f a) (inducedMeasurementSystem F g b) = ∑ α : I, ∑ β : I', c (f α) (g β) • Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (E α) (F β)

Pushing both measurements forward. The accepted operator of two induced measurements is the accepted operator of the original ones, read through the two maps.

The normalized EPR state

noncomputable def MIPRE.LCS.eprState (n : Type u_1) [Fintype n] [DecidableEq n] : n × n → ℂ

The normalized EPR state Ω / √|n|.

Equations

• MIPRE.LCS.eprState n = (↑√↑(Fintype.card n))⁻¹ • MIPRE.LCS.eprVec n

theorem MIPRE.LCS.star_eprVec_dotProduct (n : Type u_1) [Fintype n] [DecidableEq n] (v : n × n → ℂ) : star (eprVec n) ⬝ᵥ v = ∑ a : n, v (a, a)

theorem MIPRE.LCS.eprVec_form_kron (n : Type u_1) [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) : star (eprVec n) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec (eprVec n) = ∑ a : n, ∑ k : n, A a k * B a k

theorem MIPRE.LCS.eprVec_form_kron_comm (n : Type u_1) [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) : star (eprVec n) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec (eprVec n) = star (eprVec n) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B A).mulVec (eprVec n)

theorem MIPRE.LCS.eprState_form (n : Type u_1) [Fintype n] [DecidableEq n] (M : Matrix (n × n) (n × n) ℂ) : star (eprState n) ⬝ᵥ M.mulVec (eprState n) = (↑(Fintype.card n))⁻¹ * star (eprVec n) ⬝ᵥ M.mulVec (eprVec n)

theorem MIPRE.LCS.eprState_unit (n : Type u_1) [Fintype n] [DecidableEq n] [Nonempty n] : star (eprState n) ⬝ᵥ eprState n = 1

theorem MIPRE.LCS.bornProb_eprState_comm (n : Type u_1) [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) : bornProb (eprState n) A B = bornProb (eprState n) B A

The measurements of the perfect strategy

def MIPRE.LCS.BipartiteObservableStrategy.extendAssignment {G : Layout} (i : Fin G.r) (α : G.Assignment i) : Fin G.s → ZMod 2

An assignment to the variables of equation i, extended by zero to all variables.

Equations

• MIPRE.LCS.BipartiteObservableStrategy.extendAssignment i α k = if h : k ∈ G.V i then α ⟨k, h⟩ else 0

noncomputable def MIPRE.LCS.BipartiteObservableStrategy.lcsMeasurement {G : Layout} {n : Type u_1} [Fintype n] [DecidableEq n] (strat : BipartiteObservableStrategy n G) : G.Question → G.Answer → Matrix n n ℂ

The measurements both players use: at an equation, the joint measurement of its observables, answered as an assignment extended by zero; at a variable, the binary measurement of its observable.

Equations

• One or more equations did not get rendered due to their size.
• strat.lcsMeasurement (Sum.inr j) = MIPRE.LCS.inducedMeasurementSystem (MIPRE.LCS.observableToProjector (strat.obs j)) Sum.inr

theorem MIPRE.LCS.BipartiteObservableStrategy.isMeasurementSystem_lcsMeasurement {G : Layout} {n : Type u_1} [Fintype n] [DecidableEq n] (strat : BipartiteObservableStrategy n G) (x : G.Question) : IsMeasurementSystem (strat.lcsMeasurement x)

noncomputable def MIPRE.LCS.BipartiteObservableStrategy.lcsPM {G : Layout} {n : Type u_1} [Fintype n] [DecidableEq n] (strat : BipartiteObservableStrategy n G) : ProjectiveMeasurement G.Question G.Answer (Matrix n n ℂ)

The measurements as a ProjectiveMeasurement.

Equations

• strat.lcsPM = { M := strat.lcsMeasurement, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

The accepted probability as one quadratic form

theorem MIPRE.LCS.condWin_eq_re {X : Type u_2} {A : Type u_3} {m : Type u_4} [Fintype X] [Fintype A] [Fintype m] [DecidableEq m] (Γ : MIPRE.Game X X A A) (ψ : m × m → ℂ) (P : ProjectiveMeasurement X A (Matrix m m ℂ)) (x y : X) : condWin Γ ψ (fun (x : X) => P.toPOVM x) (fun (y : X) => P.toPOVM y) x y = (star ψ ⬝ᵥ (∑ a : A, ∑ b : A, (if Γ.D x y a b = true then 1 else 0) • Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P.M x a) (P.M y b)).mulVec ψ).re

theorem MIPRE.LCS.condWin_swap {X : Type u_2} {A : Type u_3} {m : Type u_4} [Fintype X] [Fintype A] [Fintype m] [DecidableEq m] (Γ : MIPRE.Game X X A A) (ψ : m × m → ℂ) (P : ProjectiveMeasurement X A (Matrix m m ℂ)) (hD : ∀ (x y : X) (a b : A), Γ.D x y a b = Γ.D y x b a) (hψ : ∀ (E F : Matrix m m ℂ), bornProb ψ E F = bornProb ψ F E) (x y : X) : condWin Γ ψ (fun (x : X) => P.toPOVM x) (fun (y : X) => P.toPOVM y) x y = condWin Γ ψ (fun (x : X) => P.toPOVM x) (fun (y : X) => P.toPOVM y) y x

Exchanging the players, for a symmetric game, a symmetric Born rule and one measurement family used by both.

theorem MIPRE.LCS.BipartiteObservableStrategy.sum_extendAssignment {G : Layout} (i : Fin G.r) (α : G.Assignment i) : ∑ k ∈ G.V i, extendAssignment i α k = ∑ k : ↥(G.V i), α k

theorem MIPRE.LCS.BipartiteObservableStrategy.extendAssignment_of_mem {G : Layout} (i : Fin G.r) (α : G.Assignment i) {j : Fin G.s} (hj : j ∈ G.V i) : extendAssignment i α j = α ⟨j, hj⟩

theorem MIPRE.LCS.BipartiteObservableStrategy.acceptedOp_eq {G : Layout} {n : Type u_1} [Fintype n] [DecidableEq n] (game : Game G) (strat : BipartiteObservableStrategy n G) (i : Fin G.r) {j : Fin G.s} (hj : j ∈ G.V i) : ∑ a : G.Answer, ∑ b : G.Answer, (if game.accepts (Sum.inl i) (Sum.inr j) a b = true then 1 else 0) • Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (strat.lcsMeasurement (Sum.inl i) a) (strat.lcsMeasurement (Sum.inr j) b) = localWinningOperator game strat.toProjectorStrategy i ⟨j, hj⟩

The accepted operator at an incidence is the local winning operator, lifted: at the question pair (equation i, variable j), the Kronecker products of the players' accepted outcomes sum to the winning operator of the edge (i, j) of the projector strategy.

theorem MIPRE.LCS.exists_tensorStrategy_value_eq_one_of_localLoss_annihilates_epr {G : Layout} (game : Game G) (hr : 0 < G.r) (hV : ∀ (i : Fin G.r), (G.V i).Nonempty) {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (strat : BipartiteObservableStrategy n G) (hLoss : ∀ (i : Fin G.r) (j : ↥(G.V i)), (localLossOperator game strat.toProjectorStrategy i j).mulVec (eprVec n) = 0) : ∃ (S : TensorProductStrategy (game.toNonlocalGame hr hV)), S.value = 1

A bipartite observable strategy whose local loss operators all annihilate the (unnormalized) EPR vector yields a perfect tensor-product strategy for the associated nonlocal game.

Both players use one measurement family (lcsMeasurement) on ℂ^n, sharing the normalized EPR state eprState n. At an equation i a player measures the joint measurement of the grid observables of i, answering the assignment extended by zero; at a variable j, the binary measurement of obs j. At an oriented incidence the Kronecker products of the accepted outcomes sum to the lifted local winning operator (acceptedOp_eq), which fixes the EPR vector because the local loss operator annihilates it; the other orientation is the same by the symmetry of the EPR state (bornProb_eprState_comm) and of the decider. The [Nonempty n] hypothesis is necessary: for empty n the hypothesis hLoss is vacuous while no unit vector exists. Blueprint thm:lcs-perfect.