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. $$
• bipartiteAliceLift_mulVec_epr_eq_zero_iff, one_sub_kronecker_mulVec_epr_eq_zero_iff, bipartiteAliceLift_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 MIPRE.LCS.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

• MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.bipartiteAliceLift_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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.bipartiteAliceLift_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 MIPRE.LCS.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 localLossOperator_sos, their square-sum, and the three extraction stages: loss kills Ω, the SOS terms kill Ω, and the local matrix identities follow.

noncomputable def MIPRE.LCS.sosConsistencyTerm {G : Layout} (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) : Matrix (n × n) (n × n) ℂ

The consistency SOS relation term.

Equations

• MIPRE.LCS.sosConsistencyTerm n strat i j = 1 - strat.bobObs ↑j * strat.aliceObs i j

noncomputable def MIPRE.LCS.sosRowTerm {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) : Matrix (n × n) (n × n) ℂ

The row-product SOS relation term.

Equations

• MIPRE.LCS.sosRowTerm game n strat i = 1 - (-1) ^ (game.b i).val • strat.aliceRowProd i

noncomputable def MIPRE.LCS.sosProductTerm {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) : Matrix (n × n) (n × n) ℂ

The product SOS relation term.

Equations

• MIPRE.LCS.sosProductTerm game n strat i j = 1 - (-1) ^ (game.b i).val • (strat.aliceRowProd i * strat.aliceObs i j * strat.bobObs ↑j)

noncomputable def MIPRE.LCS.sosSquareSum {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) : Matrix (n × n) (n × n) ℂ

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

Equations

• MIPRE.LCS.sosSquareSum game n strat i j = MIPRE.LCS.sosConsistencyTerm n strat i j ^ 2 + MIPRE.LCS.sosRowTerm game n strat i ^ 2 + MIPRE.LCS.sosProductTerm game n strat i j ^ 2

Stage 1: Local Loss ⇒ Scaled SOS Square-Sum

theorem MIPRE.LCS.local_loss_kills_epr_sos_sum {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (hLoss : (localLossOperator game strat i j).mulVec (eprVec n) = 0) : ((1 / 8) • sosSquareSum game n 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 localLossOperator_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 localLossOperator_sos.

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

theorem MIPRE.LCS.sos_sum_kills_epr_implies_terms_kill_epr {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (h : ((1 / 8) • sosSquareSum game n strat i j).mulVec (eprVec n) = 0) : (sosConsistencyTerm n strat i j).mulVec (eprVec n) = 0 ∧ (sosRowTerm game n strat i).mulVec (eprVec n) = 0 ∧ (sosProductTerm game n 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 MIPRE.LCS.consistency_of_epr_annihilates {G : Layout} (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B : Matrix n n ℂ) (hCons : (sosConsistencyTerm n strat i j).mulVec (eprVec n) = 0) (hAlice : strat.aliceObs i j = bipartiteAliceLift A) (hBob : strat.bobObs ↑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 MIPRE.LCS.row_relation_of_epr_annihilates {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (Row : Matrix n n ℂ) (hRow : (sosRowTerm game n strat i).mulVec (eprVec n) = 0) (hRowLift : strat.aliceRowProd i = bipartiteAliceLift Row) : Row = (-1) ^ (game.b i).val • 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 MIPRE.LCS.product_relation_of_epr_annihilates {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B Row : Matrix n n ℂ) (hProd : (sosProductTerm game n strat i j).mulVec (eprVec n) = 0) (hAlice : strat.aliceObs i j = bipartiteAliceLift A) (hBob : strat.bobObs ↑j = bipartiteBobLift B) (hRowLift : strat.aliceRowProd i = bipartiteAliceLift Row) : (-1) ^ (game.b i).val • (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 MIPRE.LCS.local_matrix_identities_of_sos_terms_annihilate_epr {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B Row : Matrix n n ℂ) (hCons : (sosConsistencyTerm n strat i j).mulVec (eprVec n) = 0) (hRow : (sosRowTerm game n strat i).mulVec (eprVec n) = 0) (hProd : (sosProductTerm game n strat i j).mulVec (eprVec n) = 0) (hAlice : strat.aliceObs i j = bipartiteAliceLift A) (hBob : strat.bobObs ↑j = bipartiteBobLift B) (hRowLift : strat.aliceRowProd i = bipartiteAliceLift Row) (hBobs : IsObservable B) : A = B.transpose ∧ Row = (-1) ^ (game.b i).val • 1 ∧ (-1) ^ (game.b i).val • (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 MIPRE.LCS.local_matrix_identities_of_local_loss_annihilate_epr {G : Layout} (game : Game G) (n : Type u_1) [Fintype n] [DecidableEq n] (strat : ProjectorStrategy (Matrix (n × n) (n × n) ℂ) G) (i : Fin G.r) (j : ↥(G.V i)) (A B Row : Matrix n n ℂ) (hLoss : (localLossOperator game strat i j).mulVec (eprVec n) = 0) (hAlice : strat.aliceObs i j = bipartiteAliceLift A) (hBob : strat.bobObs ↑j = bipartiteBobLift B) (hRowLift : strat.aliceRowProd i = bipartiteAliceLift Row) (hBobs : IsObservable B) : A = B.transpose ∧ Row = (-1) ^ (game.b i).val • 1 ∧ (-1) ^ (game.b i).val • (Row * A * B.transpose) = 1

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.