Landau Identity for Finite Matrix Observables

Abstract

The algebraic Landau identity for the finite-dimensional CHSH operator.

Theorem 1.1 (The CHSH square is governed by local commutators).

$$\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)\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),C:=-\mathrm{kronecker}((A_0{A}_1-A_1{A}_0),(B_0{B}_1-B_1{B}_0));S^2=4\cdot I_{m\times n}+C$$

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

Source. Repository-derived.

Commentary.

Let m and n be finite index types with decidable equality. Let A0 and A1 be Hermitian involutions in the m-by-m complex matrices, and let B0 and B1 be Hermitian involutions in the n-by-n complex matrices. For the displayed CHSH matrix S, its square is four times the identity plus C, where C is the negative Kronecker product of the two local commutators. The declaration proves this exact matrix equality. Hermiticity records the observable context, while the proof uses only the four involution equations. This is the algebraic kernel only: it introduces no state or variance, proves no positivity or norm estimate, and does not establish the three-gap decomposition, its saturation conditions, or the Tsirelson bound.

References

• Truth anchor: D5/S3/QuantumBounds/LandauIdentity.landau_identity