Strict qualitative ranking among the six fixed experiments

Open

QAlgorithms.Papers.Independent.Intakethird100.P80.qualitative_ranking

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

prove2quantum

Let $S^{\rm UC}$ denote the statistical strength with independent setting sampling for the six fixed experiments specified in Appendix III, with their states and measurement choices held fixed. Then

\max\{S^{\rm UC}_{\rm Bell\ original},S^{\rm UC}_{\rm Bell\ optimized},S^{\rm UC}_{\rm Hardy},S^{\rm UC}_{\rm Mermin}\}<S^{\rm UC}_{\rm CHSH}<S^{\rm UC}_{\rm GHZ}.

CHSH achieves its product-setting optimum with uniform sampling. This is a comparison within these six experiments; it does not assert global optimality among all bipartite quantum experiments. The paragraph's defective numerical factor is separately recorded as a deferral.

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.8–9, Section V: strict comparison ONLY among the six fixed experiments.
The defective quantitative factor in the same paragraph is separately deferred. -/
theorem qualitative_ranking :
    uncorrelatedStrength originalBell < uncorrelatedStrength chshTable ∧
    uncorrelatedStrength optimizedBell < uncorrelatedStrength chshTable ∧
    uncorrelatedStrength hardy < uncorrelatedStrength chshTable ∧
    uncorrelatedStrength mermin < uncorrelatedStrength chshTable ∧
    uncorrelatedStrength chshTable < uncorrelatedStrength ghzTable ∧
    uniformStrength chshTable = uncorrelatedStrength chshTable := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P80

end

Source

The statistical strength of nonlocality proofs, arXiv:quant-ph/0307125v2, PDF p. 9, Section V: qualitative comparison within the six fixed experiments

Read-back

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

For each table $Q$ below, its scenario has binary outcomes, with setting space $A=\prod_i A_i$ and assignment space $V=\prod_i\prod_{a\in A_i}\{0,1\}$ . Let $\Delta_A,\Delta_V$ denote their probability simplices, let $\mathcal U$ consist of setting distributions $s(a)=\prod_i s_i(a_i)$ for probability vectors $s_i$ , and put $L_p(a,x)=\sum_{v:\,\forall i,\ v_{i,a_i}=x_i}p(v)$ . For $s\in\Delta_A,p\in\Delta_V$ , define $K_Q(s,p)$ from $q(a,x)=s(a)Q(a,x)$ and $r(a,x)=s(a)L_p(a,x)$ to be $+\infty$ if some $q(a,x)>0$ has $r(a,x)=0$ , and otherwise the nonnegative part of $\sum_{a,x}q(a,x)\log_2(q(a,x)/r(a,x))$ , taking a summand to be $0$ when $q(a,x)=0$ . Define

U(Q)=\sup_{s\in\mathcal U}\inf_{p\in\Delta_V}K_Q(s,p), \qquad F(Q)=\inf_{p\in\Delta_V}K_Q(u,p), \quad u(a)=|A|^{-1},

with values in $[0,+\infty]$ . The tables called original Bell, optimized Bell, Hardy, and CHSH each have two parties and two settings per party. For the original Bell table, put $A_0=0,A_1=\pi/8$ , $B_0=\pi/8,B_1=\pi/4$ ; its value at $(a,x)$ is $\cos^2(A_{a_0}-B_{a_1})/2$ when $x_0=x_1$ and $\sin^2(A_{a_0}-B_{a_1})/2$ otherwise. The optimized Bell table has equal-outcome/unequal-outcome values $(1/2,0)$ at $a=(0,0)$ , $(1/8,3/8)$ at $a=(0,1)$ , and $(3/8,1/8)$ at the other two settings, where each value applies to each individual outcome pair of that kind. For the Hardy table, define

\alpha=\frac{\sqrt{2+2\sqrt{-13+6\sqrt5}}}{2},\qquad \beta=\sqrt{1-\alpha^2},

u_0=\sqrt{\frac{\beta}{\alpha+\beta}},\quad v_0=\sqrt{\frac{\alpha}{\alpha+\beta}},\qquad u_1=-\sqrt{\frac{\beta^3}{\alpha^3+\beta^3}},\quad v_1=\sqrt{\frac{\alpha^3}{\alpha^3+\beta^3}},

and let $(h(a,1,0),h(a,1,1))=(u_a,v_a)$ and $(h(a,0,0),h(a,0,1))=(-v_a,u_a)$ ; then its value is $\bigl(\alpha h(a_0,x_0,0)h(a_1,x_1,0)-\beta h(a_0,x_0,1)h(a_1,x_1,1)\bigr)^2$ . The CHSH table has value $1/4+\sqrt2/8$ when $(x_0\ne x_1)\iff(a_0=a_1=1)$ and $1/4-\sqrt2/8$ otherwise. The Mermin table has two parties and three settings per party, with equal-outcome/unequal-outcome values $(1/2,0)$ when $a_0=a_1$ and $(1/8,3/8)$ otherwise. The GHZ table has three parties and two settings per party: when $a_0+a_1+a_2$ is $0$ or $2$ , its value is $1/4$ if the outcome sum has odd parity at $a=(0,0,0)$ or even parity at the other such settings, and $0$ otherwise; at all remaining settings its value is $1/8$ . The declaration asserts the strict inequalities

\begin{gathered} U(Q_{\mathrm{original\ Bell}})<U(Q_{\mathrm{CHSH}}),\qquad U(Q_{\mathrm{optimized\ Bell}})<U(Q_{\mathrm{CHSH}}),\\ U(Q_{\mathrm{Hardy}})<U(Q_{\mathrm{CHSH}}),\qquad U(Q_{\mathrm{Mermin}})<U(Q_{\mathrm{CHSH}}),\qquad U(Q_{\mathrm{CHSH}})<U(Q_{\mathrm{GHZ}}), \end{gathered}

and the equality $F(Q_{\mathrm{CHSH}})=U(Q_{\mathrm{CHSH}})$ .

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