CHSH Square under Local Commutativity

Abstract

Local commutativity collapses the algebraic CHSH square to four times the identity.

Theorem 1.1 (Local commutativity collapses the CHSH square).

$$\forall m,n,[\mathrm{Fintype}(m)][\mathrm{DecidableEq}(m)][\mathrm{Fintype}(n)][\mathrm{DecidableEq}(n)],\forall A_0,A_1\in M_m(\mathbb{C}),\forall B_0,B_1\in M_n(\mathbb{C}),(\mathrm{Hermitian}(A_0)\wedge A_0^2=I_m)\wedge (\mathrm{Hermitian}(A_1)\wedge A_1^2=I_m)\wedge (\mathrm{Hermitian}(B_0)\wedge B_0^2=I_n)\wedge (\mathrm{Hermitian}(B_1)\wedge B_1^2=I_n)\wedge ((A_0{A}_1=A_1{A}_0)\vee (B_0{B}_1=B_1{B}_0))\Rightarrow \mathrm{let}S:=\mathrm{kronecker}(A_0,B_0)+\mathrm{kronecker}(A_0,B_1)+\mathrm{kronecker}(A_1,B_0)-\mathrm{kronecker}(A_1,B_1);S^2=4\cdot I_{m\times n}$$

Proof. Machine-checked in Lean as D5/S3/QuantumBounds/LandauCommutingCollapse.chsh_square_eq_four_of_local_pair_commutes (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Lawrence J. Landau (1987). On the violation of Bell’s inequality in quantum theory. DOI: 10.1016/0375-9601(87)90075-2.

Commentary.

Let A0 and A1 and B0 and B1 be finite complex Hermitian involutions. If either the Alice pair or the Bob pair commutes, then the square of their CHSH matrix is four times the identity. The proof specializes LandauIdentity.landau_identity: the local commutation equality makes one commutator, and hence their Kronecker product, zero.

The acknowledged article’s full text was not readable, so this repository-derived provenance does not claim that the article states this exact commuting-pair corollary.

This is only the algebraic square equality under a commuting local pair. It does not assert an expectation bound of two, an operator-norm CHSH bound of two, or any optimization over states.

References

• Truth anchor: D5/S3/QuantumBounds/LandauCommutingCollapse.chsh_square_eq_four_of_local_pair_commutes
• Dependency: D5/S3/QuantumBounds/LandauIdentity