Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing CHSH Rigidity in Lean 4

Tianrun Zhao, Nengkun Yu

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

Formalizing CHSH Rigidity in Lean 4

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

Paper Structure

This paper contains 19 sections, 1 theorem, 37 equations.

Table of Contents

  1. Introduction
  2. A Gap in the Original Literature
  3. Concrete counterexample (in dimension 2).
  4. Comment
  5. Rigidity and Self-Testing
  6. Bell states.
  7. CHSH operators and strategies.
  8. Abstract CHSH strategy.
  9. Tsirelson's bound.
  10. Canonical two-qubit model.
  11. Spectral decomposition.
  12. Robust rigidity of CHSH
  13. Proof
  14. Formalization of robust CHSH rigidity
  15. Representative Lean 4 declarations.
  16. ...and 4 more sections

Key Result

Theorem 3.1

Let $S = (|\psi\rangle, A_0, A_1, B_0, B_1)$ be an entangled strategy for the CHSH game. Let $\varepsilon\ge 0$ be sufficiently small, suppose the bias satisfies Then there exist local isometries $V_A:H_A\to \mathbb{C}^2\otimes H_A$ and $V_B:H_B\to \mathbb{C}^2\otimes H_B$ and a state $|\Phi_{\text{junk}}\rangle\in H_A\otimes H_B$ such that: $\blacktriangleleft$$\blacktriangleleft$

Theorems & Definitions (2)

  • Theorem 3.1: Robust CHSH rigidity cleve2019qic890
  • proof : Proof Sketch