Formalizing CHSH Rigidity in Lean 4
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911567831891968 |
|---|---|
| author | Zhao, Tianrun Yu, Nengkun |
| author_facet | Zhao, Tianrun Yu, Nengkun |
| contents | 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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_03884 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formalizing CHSH Rigidity in Lean 4 Zhao, Tianrun Yu, Nengkun Quantum Physics Logic in Computer Science 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). |
| title | Formalizing CHSH Rigidity in Lean 4 |
| topic | Quantum Physics Logic in Computer Science |
| url | https://arxiv.org/abs/2604.03884 |