{"id":"palomar/PALOMAR-2026-08-19-000007","url":"https://github.com/stalex444/pdt-lean/tree/0dae307fb786a3d180bba137a44555a1bf645637","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-19-000007-v2.json","repo":"https://github.com/stalex444/pdt-lean","tags":["quant-ph","math.OA","msc:81P40","msc:81P45","msc:46L60","msc:15A18","quantum-info","chsh-inequality","operator-algebras","lean-formalization"],"score":0,"title":"stalex444/pdt-lean","trust":"high","domain":"quant-ph","source":"palomar","authors":["Stephanie Alexander"],"reviews":0,"subject":"quant-ph","summary":"Kernel-checked exact-constant results for the CHSH operator T = A₀B₀ + A₀B₁ + A₁B₀ − A₁B₁ of an arbitrary CHSH tuple (Mathlib's IsCHSHTuple: self-adjoint involutions with the A's commuting with the B's). (1) The Landau identity: in any *-ring, T² = 4 + [A₀,A₁]·[B₁,B₀] — the exact, representation-independent correction to the naive T² = 8·1 (chsh_mul_self). (2) Tsirelson's bound in norm form: ‖T‖ ≤ 2√2 for every CHSH tuple in every nontrivial unital real C*-normed algebra (chsh_norm_le). (3) The classical constant, exactly: if either party's pair commutes, ‖T‖ = 2 — not merely ≤ 2…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true,"formalizes":[{"title":"Quantum generalizations of Bell's inequality","identifier":"Letters in Mathematical Physics 4 (1980), 93–100","relationship":"formalizes"},{"title":"On the violation of Bell's inequality in quantum theory","identifier":"Physics Letters A 120, no. 2 (1987), 54–56","relationship":"formalizes"}]}