Nonlocality and certification / Bound
Tsirelson upper bound for CHSH quantum realizations
Bound statement
For every finite-dimensional tensor-product quantum realization of the two-input, two-output CHSH scenario, let $S$ be its CHSH value computed from the four signed outcome-probability correlators. Then
\[
S \le 2\sqrt{2}.
\]
Sources
- Bell nonlocality
Nicolas Brunner, Daniel Cavalcanti, Stefano Pironio, Valerio Scarani, Stephanie Wehner, 2013
Lean context
- Import
QIT.Nonlocality.Tsirelson- Lean declaration
QIT.Bell.QuantumRealization.chshValue_le_two_mul_sqrt_two
Copy a short prompt with the import, Lean declaration, citations, and public source link.