Formalizing CHSH Rigidity in Lean 4

TL;DR

This paper formalizes the CHSH rigidity theorem in Lean 4, proving that near-optimal strategies are essentially equivalent to canonical qubit strategies, and identifies a gap in prior proofs.

Contribution

It provides a formal proof of the CHSH rigidity theorem in Lean 4 and uncovers a gap in previous related arguments.

Findings

Formal proof of CHSH rigidity theorem in Lean 4

Identification of a gap in McKague, Yang, and Scarani's argument

Clarification of the structure of near-optimal quantum strategies

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).