Formalizing CHSH Rigidity in Lean 4
arXiv:2604.0388485.7h-index: 3
AI Analysis
Provides a fully verified formal proof of a foundational quantum information theorem, addressing correctness for the community.
The authors formalized the CHSH rigidity theorem in Lean 4, proving that near-optimal CHSH strategies are locally isometric to the canonical qubit strategy, and identified a gap in a prior proof.
Violation of the Clauser-Horne-Shimony-Holt (CHSH) inequality certifies genuine quantum correlations. In this work, we formalize in Lean 4 the rigidity theorem -- any strategy achieving near-optimal CHSH value must be locally isometric to the canonical qubit strategy. In the course of formalization, we identified a gap in the argument of McKague, Yang, and Scarani (arXiv:1203.2976).