Formalizing CHSH Rigidity in Lean 4
Quantum Physics
2026-04-07 v1 Logic in Computer Science
Abstract
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).
Cite
@article{arxiv.2604.03884,
title = {Formalizing CHSH Rigidity in Lean 4},
author = {Tianrun Zhao and Nengkun Yu},
journal= {arXiv preprint arXiv:2604.03884},
year = {2026}
}