# Formalizing CHSH Rigidity in Lean 4

Preprint · Tianrun Zhao, Nengkun Yu

- Archive id: arxiv:2604.03884
- Published: 2026-04-04
- arXiv: https://arxiv.org/abs/2604.03884
- Source URL: https://arxiv.org/abs/2604.03884
- PDF: https://arxiv.org/pdf/2604.03884
- Provenance: arxiv

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

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.