Formalizing CHSH Rigidity in Lean 4

Quantum Physics [Submitted on 4 Apr 2026] Formalizing CHSH Rigidity in Lean 4 Tianrun Zhao, Nengkun Yu 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). Subjects: Quantum Physics (quant-ph); Logic in Computer Science (cs.LO) Cite as: arXiv:2604.03884 [quant-ph]   (or arXiv:2604.03884v1 [quant-ph] for this version)   https://doi.org/10.48550/arXiv.2604.03884 Focus to learn more Submission history From: Tianrun Zhao [view email] [v1] Sat, 4 Apr 2026 22:31:36 UTC (1,519 KB) Access Paper: view license Current browse context: quant-ph < prev   |   next > new | recent | 2026-04 Change to browse by: cs cs.LO References & Citations INSPIRE HEP NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)