Exact CHSH saddle point and all three strengths

Open

QAlgorithms.Papers.Independent.Intakethird100.P80.chsh_strength

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For the fixed CHSH experiment, outcomes are $T,F$ and the three settings $11,12,21$ favor equal outcomes, while $22$ favors unequal outcomes. Each favored outcome has probability $h=(2+\sqrt2)/8$ and each other outcome has probability $\ell=(2-\sqrt2)/8$ . Let $\widetilde\pi$ put probability $1/8$ on each assignment $FFFF,TTTT,FFFT,TTTF,FFTF,TTFT,TFFT,FTTF$ in coordinate order $(x_1,x_2,y_1,y_2)$ , and zero on all others. Let $\widetilde\sigma$ be uniform on the four settings.

The pair $(\widetilde\sigma,\widetilde\pi)$ is a saddle point in both the correlated and product games. The local strategy is an equalizer, and

S^{\rm UNI}_{\rm CHSH}=S^{\rm UC}_{\rm CHSH}=S^{\rm COR}_{\rm CHSH}=D_2(Q_{\widetilde\sigma}\|P_{\widetilde\sigma;\widetilde\pi})=2h\log_2\frac{h}{3/8}+2\ell\log_2\frac{\ell}{1/8}.

This evaluates the strength of this specified experiment, without optimizing quantum states or measurement directions.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P80

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P80

open scoped BigOperators ENNReal Topology Classical

open MeasureTheory Filter

/-- PDF pp.6,9,14–15,18,21: the specified CHSH saddle and all three EXACT strengths.
The decimal 0.0462738469 is not asserted as an exact value. -/
theorem chsh_strength :
    chshLocal ∈ stdSimplex ℝ (Potential BellScenario) ∧
    Saddle chshTable (stdSimplex ℝ (Settings BellScenario)) (uniformSettings BellScenario) chshLocal ∧
    Saddle chshTable (productSettings BellScenario) (uniformSettings BellScenario) chshLocal ∧
    (∀ s : Sigma BellScenario, statisticalPayoff chshTable s.1 chshLocal =
      statisticalPayoff chshTable (uniformSettings BellScenario) chshLocal) ∧
    uniformStrength chshTable = uncorrelatedStrength chshTable ∧
    uncorrelatedStrength chshTable = correlatedStrength chshTable ∧
    correlatedStrength chshTable = statisticalPayoff chshTable (uniformSettings BellScenario) chshLocal ∧
    correlatedStrength chshTable = ENNReal.ofReal (
      2 * (1 / 4 + Real.sqrt 2 / 8) * Real.logb 2 ((1 / 4 + Real.sqrt 2 / 8) / (3 / 8)) +
      2 * (1 / 4 - Real.sqrt 2 / 8) * Real.logb 2 ((1 / 4 - Real.sqrt 2 / 8) / (1 / 8))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P80

end

Source

The statistical strength of nonlocality proofs, arXiv:quant-ph/0307125v2, PDF p. 6, Example 4 and Appendix III-C: exact CHSH saddle point and all three strengths

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Consider two parties, each with settings and outcomes in $\{0,1\}$ . Write $a=(a_0,a_1)$ for a setting pair, $x=(x_0,x_1)$ for an outcome pair, and $v=(v_{00},v_{01},v_{10},v_{11})$ for an assignment of an outcome to each party’s every setting. Let $\Delta_A$ and $\Delta_V$ be the probability simplices on setting pairs and such assignments, respectively, and let $\mathcal U\subseteq\Delta_A$ consist of distributions $s(a)=s_0(a_0)s_1(a_1)$ for some probability vectors $s_0,s_1$ . Define $u(a)=1/4$ , and define $p_*(v)=1/8$ on the eight assignments

(0,0,0,0),\ (1,1,1,1),\ (0,0,0,1),\ (1,1,1,0),\ (0,0,1,0),\ (1,1,0,1),\ (1,0,0,1),\ (0,1,1,0),

with $p_*(v)=0$ otherwise. Put $\eta=1/4+\sqrt2/8$ and $\zeta=1/4-\sqrt2/8$ , and define $Q(a,x)=\eta$ if $(x_0\ne x_1)\iff(a_0=a_1=1)$ , and $Q(a,x)=\zeta$ otherwise. For an assignment distribution $p$ , let $L_p(a,x)=\sum_{v:\,v_{0a_0}=x_0,\ v_{1a_1}=x_1}p(v)$ . For $s\in\Delta_A$ and $p\in\Delta_V$ , define $K(s,p)$ by setting $q(a,x)=s(a)Q(a,x)$ and $r(a,x)=s(a)L_p(a,x)$ : its value is $+\infty$ if some $(a,x)$ satisfies $q(a,x)>0$ and $r(a,x)=0$ , and otherwise it is

K(s,p)=\max\!\left\{0,\ \sum_{a,x} \begin{cases} 0,&q(a,x)=0,\\ q(a,x)\log_2\!\bigl(q(a,x)/r(a,x)\bigr),&q(a,x)\ne0 \end{cases}\right\},

viewed in $[0,+\infty]$ . Define $F=\inf_{p\in\Delta_V}K(u,p)$ , $U=\sup_{s\in\mathcal U}\inf_{p\in\Delta_V}K(s,p)$ , and $C=\sup_{s\in\Delta_A}\inf_{p\in\Delta_V}K(s,p)$ . The declaration asserts that $p_*\in\Delta_V$ ; for each of the two choices $\mathcal A=\Delta_A$ and $\mathcal A=\mathcal U$ , one has $u\in\mathcal A$ , $p_*\in\Delta_V$ , $K(t,p_*)\le K(u,p_*)$ for every $t\in\mathcal A$ , and $K(u,p_*)\le K(u,p)$ for every $p\in\Delta_V$ ; moreover, $K(s,p_*)=K(u,p_*)$ for every $s\in\Delta_A$ , and

F=U,\qquad U=C,\qquad C=K(u,p_*),\qquad C=\max\!\left\{0,\, 2\eta\log_2\!\frac{\eta}{3/8} +2\zeta\log_2\!\frac{\zeta}{1/8}\right\}.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph