The CHSH rigidity theorem is machine-checked in Lean 4, confirming near-optimal strategies are locally isometric to the qubit strategy while exposing a gap in prior reasoning.
Qic 890 entanglement and nonlocal effects, April 2019
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
quant-ph 1years
2026 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
Formalizing CHSH Rigidity in Lean 4
The CHSH rigidity theorem is machine-checked in Lean 4, confirming near-optimal strategies are locally isometric to the qubit strategy while exposing a gap in prior reasoning.