Winning Condition and Loss Operators

This module defines the operator-valued winning and loss expressions attached to an LCS game and a projector strategy.

Its main result is a sum-of-squares decomposition of the local loss operator, following the paper's algebraic winning-condition identities.

Local Operators

This section defines the winning assignments for a constraint and the associated local winning and loss operators.

def MIPRE.LCS.winningAssignments {G : Layout} (game : Game G) (i : Fin G.r) : Finset (G.Assignment i)

The assignments satisfying equation i in the game game.

Equations

• MIPRE.LCS.winningAssignments game i = {α : G.Assignment i | ∑ j : ↥(G.V i), α j = game.b i}

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

The local winning operator for a single edge (i, j).

Equations

• MIPRE.LCS.localWinningOperator game strat i j = ∑ x ∈ MIPRE.LCS.winningAssignments game i, strat.E i x * strat.F (↑j) (x j)

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

The local loss operator for a single edge (i, j).

Equations

• MIPRE.LCS.localLossOperator game strat i j = 1 - MIPRE.LCS.localWinningOperator game strat i j

Winning Projector Identities

Two local projector identities used in the sum-of-squares derivation.

theorem MIPRE.LCS.sum_winning_projectors_eq_row_observable {G : Layout} (game : Game G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : ProjectorStrategy R G) (i : Fin G.r) : ∑ x ∈ winningAssignments game i, strat.E i x = (1 / 2) • (1 + (-1) ^ (game.b i).val • strat.aliceRowProd i)

Lemma 4.7.1: the sum of winning projectors equals the signed row-product expression.

theorem MIPRE.LCS.sum_marginal_projectors_eq_half_one_add_aliceObs {G : Layout} {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) (y : ZMod 2) : ∑ x : G.Assignment i with x j = y, strat.E i x = (1 / 2) • (1 + (-1) ^ y.val • strat.aliceObs i j)

Lemma 4.7.2: the marginal projector sum equals the signed local observable expression.

Local Loss SOS

This section derives the sum-of-squares decomposition of the local loss operator by a sequence of private rewriting lemmas.

theorem MIPRE.LCS.localLossOperator_sos {G : Layout} (game : Game G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : ProjectorStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : localLossOperator game strat i j = (1 / 8) • ((1 - strat.bobObs ↑j * strat.aliceObs i j) ^ 2 + (1 - (-1) ^ (game.b i).val • strat.aliceRowProd i) ^ 2 + (1 - (-1) ^ (game.b i).val • (strat.aliceRowProd i * strat.aliceObs i j * strat.bobObs ↑j)) ^ 2)

The Sum of Squares decomposition of the local loss operator.

Global Operators

The overall winning and loss operators are obtained by averaging the local quantities over the question graph of the game.

noncomputable def MIPRE.LCS.winningOperator {G : Layout} (game : Game G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : ProjectorStrategy R G) : R

The total winning operator v is the average of the local winning operators.

Equations

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

noncomputable def MIPRE.LCS.lossOperator {G : Layout} (game : Game G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : ProjectorStrategy R G) : R

The total Loss Operator 1 - v.

Equations

• MIPRE.LCS.lossOperator game strat = 1 - MIPRE.LCS.winningOperator game strat