EPR Extraction for LCS Relation Terms

This module contains the EPR/vectorization algebra and SOS extraction lemmas used to turn perfect local LCS play into local matrix identities. The EPR vector is intentionally unnormalized: $$ \Omega = \sum_a e_a \otimes e_a, $$ since the arguments only use annihilation and injectivity.

The basic EPR identities are:

• kronecker_mulVec_epr, computing the action of a two-sided Kronecker product: $$ ((M \otimes N)\Omega)_{a,b} = \sum_k M_{a,k}N_{b,k}. $$
• kronecker_mulVec_epr_eq_zero_iff, converting EPR annihilation into the local matrix equation $$ (M \otimes N)\Omega = 0 \quad\Longleftrightarrow\quad MN^T = 0. $$
• alice_lift_mulVec_epr_eq_zero_iff, one_sub_kronecker_mulVec_epr_eq_zero_iff, alice_lift_one_sub_smul_mulVec_epr_eq_zero_iff, and one_sub_smul_kronecker_mulVec_epr_eq_zero_iff, which are the specialized injectivity forms used for bipartite Alice/Bob lifts.

The LCS-specific part defines the three SOS relation terms sosConsistencyTerm, sosRowTerm, and sosProductTerm, together with their square-sum sosSquareSum. The extraction pipeline is:

• local_loss_kills_epr_sos_sum: a local loss operator killing $\Omega$ rewrites to the scaled SOS square-sum killing $\Omega$.
• sos_sum_kills_epr_implies_terms_kill_epr: positivity for self-adjoint squares gives the three individual relation annihilations.
• consistency_of_epr_annihilates, row_relation_of_epr_annihilates, and product_relation_of_epr_annihilates: the EPR identities remove $\Omega$ and produce the corresponding local matrix equations.
• local_matrix_identities_of_local_loss_annihilate_epr: the final bundled theorem, extracting all three local matrix identities directly from local-loss annihilation on $\Omega$.

The Unnormalized EPR Vector

The vector eprVec n is the coordinate function of $\Omega = \sum_{a : n} e_a \otimes e_a$.

noncomputable def eprVec (n : Type u_1) [Fintype n] [DecidableEq n] : n × n → ℂ

The unnormalized EPR vector $\Omega = \sum_a e_a \otimes e_a$, as a function on pairs.

Equations

• eprVec n ab = if ab.1 = ab.2 then 1 else 0

Kronecker Products Acting on EPR

This section proves the two core matrix identities. The first computes the action of a two-sided Kronecker product on $\Omega$. The second converts annihilation of $\Omega$ into the local matrix equation $M N^T = 0$.

theorem kronecker_mulVec_epr (n : Type u_1) [Fintype n] [DecidableEq n] (M N : Matrix n n ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N).mulVec (eprVec n) = fun (ab : n × n) => ∑ k : n, M ab.1 k * N ab.2 k

Action of a two-sided Kronecker product on the unnormalized EPR vector: $$ ((M \otimes N)\Omega)_{a,b} = \sum_k M_{a,k} N_{b,k}. $$

theorem kronecker_mulVec_epr_eq_zero_iff (n : Type u_1) [Fintype n] [DecidableEq n] (M N : Matrix n n ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N).mulVec (eprVec n) = 0 ↔ M * N.transpose = 0

The EPR vector turns two-sided annihilation into a local matrix identity: $$ (M \otimes N)\Omega = 0 \quad\Longleftrightarrow\quad M N^T = 0. $$

theorem alice_lift_mulVec_epr_eq_zero_iff (n : Type u_1) [Fintype n] [DecidableEq n] (M : Matrix n n ℂ) : (bipartiteAliceLift M).mulVec (eprVec n) = 0 ↔ M = 0

A matrix acting on Alice's side annihilates EPR iff the matrix is zero: $$ (M \otimes I)\Omega = 0 \quad\Longleftrightarrow\quad M = 0. $$

theorem one_sub_kronecker_mulVec_epr_eq_zero_iff (n : Type u_1) [Fintype n] [DecidableEq n] (M N : Matrix n n ℂ) : (1 - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N).mulVec (eprVec n) = 0 ↔ M * N.transpose = 1

The relation term $1 - M \otimes N$ annihilates EPR precisely when $$ M N^T = I. $$

Algebra of Bipartite Lifts

The observable strategy files define Alice and Bob lifts as $A \otimes I$ and $I \otimes B$. This section records the small collection of rewrite lemmas needed to turn global bipartite relation terms into local matrix equations.

theorem bipartiteBobLift_mul_bipartiteAliceLift (n : Type u_1) [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) : bipartiteBobLift B * bipartiteAliceLift A = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B

Multiplying Bob's lift by Alice's lift gives the two-sided Kronecker product: $$ (I \otimes B)(A \otimes I) = A \otimes B. $$

theorem bipartiteAliceLift_mul (n : Type u_1) [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) : bipartiteAliceLift A * bipartiteAliceLift B = bipartiteAliceLift (A * B)

Alice lifts preserve multiplication: $$ (A \otimes I)(B \otimes I) = (AB) \otimes I. $$

theorem bipartiteAliceLift_mul_bipartiteBobLift (n : Type u_1) [Fintype n] [DecidableEq n] (A B : Matrix n n ℂ) : bipartiteAliceLift A * bipartiteBobLift B = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B

Multiplying Alice's lift by Bob's lift gives the two-sided Kronecker product: $$ (A \otimes I)(I \otimes B) = A \otimes B. $$

theorem bipartiteAliceLift_one_sub_smul (n : Type u_1) [Fintype n] [DecidableEq n] (c : ℂ) (M : Matrix n n ℂ) : bipartiteAliceLift (1 - c • M) = 1 - c • bipartiteAliceLift M

Alice lifting commutes with the affine expression $1 - cM$: $$ (1 - cM) \otimes I = 1 - c (M \otimes I). $$

theorem alice_lift_one_sub_smul_mulVec_epr_eq_zero_iff (n : Type u_1) [Fintype n] [DecidableEq n] (c : ℂ) (M : Matrix n n ℂ) : (1 - c • bipartiteAliceLift M).mulVec (eprVec n) = 0 ↔ 1 - c • M = 0

EPR injectivity for an affine Alice-side relation: $$ (1 - c(M \otimes I))\Omega = 0 \quad\Longleftrightarrow\quad 1 - cM = 0. $$

theorem one_sub_smul_kronecker_mulVec_epr_eq_zero_iff (n : Type u_1) [Fintype n] [DecidableEq n] (c : ℂ) (M N : Matrix n n ℂ) : (1 - c • Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N).mulVec (eprVec n) = 0 ↔ c • (M * N.transpose) = 1

EPR injectivity for a scalar multiple of a two-sided Kronecker product: $$ (1 - c(M \otimes N))\Omega = 0 \quad\Longleftrightarrow\quad c(MN^T) = I. $$

SOS Relation Terms and Main EPR Pipeline

This section packages the three relation terms from local_loss_sos, their square-sum, and the three extraction stages: loss kills Ω, the SOS terms kill Ω, and the local matrix identities follow.

noncomputable def sosConsistencyTerm {G : LCSLayout} {m : Type u_2} [Fintype m] [DecidableEq m] (strat : LCSStrategy (Matrix m m ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) : Matrix m m ℂ

The consistency SOS relation term.

Equations

• sosConsistencyTerm strat i j = 1 - Bob_B strat ↑j * Alice_A strat i j

noncomputable def sosRowTerm {G : LCSLayout} {m : Type u_2} [Fintype m] [DecidableEq m] (game : LCSGame G) (strat : LCSStrategy (Matrix m m ℂ) G) (i : Fin G.r) : Matrix m m ℂ

The row-product SOS relation term.

Equations

• sosRowTerm game strat i = 1 - (-1) ^ ↑(game.b i) • Alice_Row_Prod strat i

noncomputable def sosProductTerm {G : LCSLayout} {m : Type u_2} [Fintype m] [DecidableEq m] (game : LCSGame G) (strat : LCSStrategy (Matrix m m ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) : Matrix m m ℂ

The product SOS relation term.

Equations

• sosProductTerm game strat i j = 1 - (-1) ^ ↑(game.b i) • (Alice_Row_Prod strat i * Alice_A strat i j * Bob_B strat ↑j)

noncomputable def sosSquareSum {G : LCSLayout} {m : Type u_2} [Fintype m] [DecidableEq m] (game : LCSGame G) (strat : LCSStrategy (Matrix m m ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) : Matrix m m ℂ

The sum of squares appearing in the local-loss SOS decomposition.

Equations

• sosSquareSum game strat i j = sosConsistencyTerm strat i j ^ 2 + sosRowTerm game strat i ^ 2 + sosProductTerm game strat i j ^ 2

Stage 1: Local Loss ⇒ Scaled SOS Square-Sum

theorem local_loss_kills_epr_sos_sum {G : LCSLayout} (game : LCSGame G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (hLoss : (local_loss_operator game strat i j).mulVec (eprVec n) = 0) : ((1 / 8) • sosSquareSum game strat i j).mulVec (eprVec n) = 0

The part of the SOS pipeline that is purely a rewrite: if the local loss annihilates EPR, then the SOS expression from local_loss_sos annihilates EPR. Extracting each individual square term from this sum requires a positivity/norm argument.

In symbols, this is the formal rewrite step $$ L_{ij}\Omega = 0 \quad\Longrightarrow\quad \frac18\,(T_1^2 + T_2^2 + T_3^2)\Omega = 0, $$ where the three $T_k$ are the SOS relation terms from local_loss_sos.

Stage 2: Scaled SOS Square-Sum ⇒ Individual SOS-Term Annihilation

theorem sos_sum_kills_epr_implies_terms_kill_epr {G : LCSLayout} (game : LCSGame G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (h : ((1 / 8) • sosSquareSum game strat i j).mulVec (eprVec n) = 0) : (sosConsistencyTerm strat i j).mulVec (eprVec n) = 0 ∧ (sosRowTerm game strat i).mulVec (eprVec n) = 0 ∧ (sosProductTerm game strat i j).mulVec (eprVec n) = 0

If the scaled SOS square-sum annihilates EPR, then each individual SOS relation term annihilates EPR: $$ \frac18(T_1^2 + T_2^2 + T_3^2)\Omega = 0 \quad\Longrightarrow\quad T_1\Omega = T_2\Omega = T_3\Omega = 0 . $$ Here $T_1 = 1 - B_jA_{ij}$, $T_2 = 1 - (-1)^{b_i}\operatorname{Row}_i(A)$, and $T_3 = 1 - (-1)^{b_i}\operatorname{Row}_i(A)A_{ij}B_j$. This is the positivity step that bridges the rewritten local-loss SOS identity from Stage 1 to the concrete local matrix identities extracted in Stage 3.

Stage 3: Individual SOS-Term Annihilation ⇒ Local Matrix Identities

The sum-of-squares decomposition produces three relation terms. Once a positivity argument shows that each term annihilates the EPR vector, the lemmas in this section remove $\Omega$ and produce the local matrix identities needed for the solution-group representation.

theorem consistency_of_epr_annihilates {G : LCSLayout} (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B : Matrix n n ℂ) (hCons : (sosConsistencyTerm strat i j).mulVec (eprVec n) = 0) (hAlice : Alice_A strat i j = bipartiteAliceLift A) (hBob : Bob_B strat ↑j = bipartiteBobLift B) (hBobs : IsObservable B) : A = B.transpose

If the consistency SOS relation annihilates EPR, the local Alice and Bob matrices agree up to transpose: $$ A_{ij} = B_j^T. $$

theorem row_relation_of_epr_annihilates {G : LCSLayout} (game : LCSGame G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (Row : Matrix n n ℂ) (hRow : (sosRowTerm game strat i).mulVec (eprVec n) = 0) (hRowLift : Alice_Row_Prod strat i = bipartiteAliceLift Row) : Row = (-1) ^ ↑(game.b i) • 1

If the row SOS relation annihilates EPR, the corresponding local row product satisfies the LCS row equation: $$ R_i = (-1)^{b_i} I. $$

theorem product_relation_of_epr_annihilates {G : LCSLayout} (game : LCSGame G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B Row : Matrix n n ℂ) (hProd : (sosProductTerm game strat i j).mulVec (eprVec n) = 0) (hAlice : Alice_A strat i j = bipartiteAliceLift A) (hBob : Bob_B strat ↑j = bipartiteBobLift B) (hRowLift : Alice_Row_Prod strat i = bipartiteAliceLift Row) : (-1) ^ ↑(game.b i) • (Row * A * B.transpose) = 1

If the third SOS relation annihilates EPR, the corresponding local product identity holds: $$ (-1)^{b_i} R_i A_{ij} B_j^T = I. $$

theorem local_matrix_identities_of_sos_terms_annihilate_epr {G : LCSLayout} (game : LCSGame G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B Row : Matrix n n ℂ) (hCons : (sosConsistencyTerm strat i j).mulVec (eprVec n) = 0) (hRow : (sosRowTerm game strat i).mulVec (eprVec n) = 0) (hProd : (sosProductTerm game strat i j).mulVec (eprVec n) = 0) (hAlice : Alice_A strat i j = bipartiteAliceLift A) (hBob : Bob_B strat ↑j = bipartiteBobLift B) (hRowLift : Alice_Row_Prod strat i = bipartiteAliceLift Row) (hBobs : IsObservable B) : A = B.transpose ∧ Row = (-1) ^ ↑(game.b i) • 1 ∧ (-1) ^ ↑(game.b i) • (Row * A * B.transpose) = 1

Bundled extraction of the local matrix identities from the individual SOS relation terms annihilating EPR.

Given annihilation of the consistency, row, and product SOS terms, this returns the three local identities $$ A_{ij} = B_j^T,\qquad R_i = (-1)^{b_i} I,\qquad (-1)^{b_i} R_i A_{ij} B_j^T = I. $$

theorem local_matrix_identities_of_local_loss_annihilate_epr {G : LCSLayout} (game : LCSGame G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : LCSStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B Row : Matrix n n ℂ) (hLoss : (local_loss_operator game strat i j).mulVec (eprVec n) = 0) (hAlice : Alice_A strat i j = bipartiteAliceLift A) (hBob : Bob_B strat ↑j = bipartiteBobLift B) (hRowLift : Alice_Row_Prod strat i = bipartiteAliceLift Row) (hBobs : IsObservable B) : A = B.transpose ∧ Row = (-1) ^ ↑(game.b i) • 1 ∧ (-1) ^ ↑(game.b i) • (Row * A * B.transpose) = 1

Final Bundle: Local Loss Annihilation on EPR ⇒ Local Matrix Identities

Final bundled extraction from local-loss annihilation on EPR to the local matrix identities.

This packages the three stages:

1. local loss annihilates Ω, so the scaled SOS square-sum annihilates Ω;
2. the positivity argument extracts annihilation of each SOS relation term;
3. EPR injectivity converts those annihilations into local matrix identities.