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 winning_assignments {G : LCSLayout} (game : LCSGame G) (i : Fin G.r) : Finset (Assignment G i)

The assignments satisfying equation i in the game game.

Equations

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

noncomputable def local_winning_operator {G : LCSLayout} (game : LCSGame G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : R

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

Equations

• local_winning_operator game strat i j = ∑ x ∈ winning_assignments game i, strat.E i x * strat.F (↑j) (x j)

noncomputable def local_loss_operator {G : LCSLayout} (game : LCSGame G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : R

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

Equations

• local_loss_operator game strat i j = 1 - local_winning_operator game strat i j

Winning Projector Identities

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

theorem sum_winning_projectors_eq_row_observable {G : LCSLayout} (game : LCSGame G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (strat : LCSStrategy R G) (i : Fin G.r) : ∑ x ∈ winning_assignments game i, strat.E i x = (1 / 2) • (1 + (-1) ^ ↑(game.b i) • (G.V i).attach.noncommProd (fun (j : { x : Fin G.s // x ∈ G.V i }) => Alice_A strat i j) ⋯)

Lemma 4.7.1 From the paper

theorem sum_marginal_projectors_eq_half_one_add_A {G : LCSLayout} {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) (y : Fin 2) : ∑ x : Assignment G i with x j = y, strat.E i x = (1 / 2) • (1 + (-1) ^ ↑y • Alice_A strat i j)

Lemma 4.7.2 From the paper

Local Loss SOS

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

theorem local_loss_sos {G : LCSLayout} (game : LCSGame G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (strat : LCSStrategy R G) (i : Fin G.r) (j : ↥(G.V i)) : local_loss_operator game strat i j = (1 / 8) • ((1 - Bob_B strat ↑j * Alice_A strat i j) ^ 2 + (1 - (-1) ^ ↑(game.b i) • Alice_Row_Prod strat i) ^ 2 + (1 - (-1) ^ ↑(game.b i) • (Alice_Row_Prod strat i * Alice_A strat i j * Bob_B strat ↑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 winning_operator {G : LCSLayout} (game : LCSGame G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : LCSStrategy R G) : R

The total Winning Operator v is the average of local winning probabilities.

Equations

• winning_operator game strat = ∑ i : Fin G.r, ∑ j : ↥(G.V i), have normalization := ↑(G.r * (G.V i).card); (1 / normalization) • local_winning_operator game strat i j

noncomputable def loss_operator {G : LCSLayout} (game : LCSGame G) {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (strat : LCSStrategy R G) : R

The total Loss Operator 1 - v.

Equations

• loss_operator game strat = 1 - winning_operator game strat