Exact GHZ strengths and optimal sampling laws

Open

QAlgorithms.Papers.Independent.Intakethird100.P80.ghz_strength

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

prove2quantum

Use the fixed GHZ experiment of Appendix III-F. On settings $111,122,212,221$ , four allowed parity outcomes have probability $1/4$ each: the number of $T$ outcomes is odd at $111$ and even at the other three settings. At all other settings every outcome has probability $1/8$ . Let $\sigma^\circ$ sample all eight settings uniformly and let $\sigma^*$ assign probability $1/4$ to each of the four parity settings.

The uniform law is optimal among product setting laws, while $\sigma^*$ is optimal among all setting laws, and

S^{\rm UNI}_{\rm GHZ}=S^{\rm UC}_{\rm GHZ}=\tfrac12\log_2(4/3),\qquad S^{\rm COR}_{\rm GHZ}=\log_2(4/3).

A single local law realizes Table XXIX at every setting: its probabilities at a parity setting are $3/16$ on allowed outcomes and $1/16$ on the others, and are $1/8$ at other settings. This law is optimal for both displayed setting laws.

The four settings and the $1/4$ masses follow Table XXVIII and equation (35); the p.24 prose mistakenly prints $(0.125,0)$ and an even number of setting-1 measurements. This statement corrects those two typos and makes no factor-4.5 comparison.

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,17,21,24: exact GHZ optima, optimal setting laws and a common realizing
local law for Table XXIX. The p.24 prose typos are corrected as documented above.
No equality or literal lower bound with the factor 4.5 is claimed. -/
theorem ghz_strength :
    ghzCorrelatedSettings ∈ stdSimplex ℝ (Settings GHZScenario) ∧
    Uncorrelated (uniformSettings GHZScenario) ∧
    uniformStrength ghzTable = uncorrelatedStrength ghzTable ∧
    uncorrelatedStrength ghzTable = ENNReal.ofReal (Real.logb 2 (4 / 3) / 2) ∧
    lowerValue ghzTable ghzCorrelatedSettings = correlatedStrength ghzTable ∧
    correlatedStrength ghzTable = ENNReal.ofReal (Real.logb 2 (4 / 3)) ∧
    ∃ p : PiLocal GHZScenario, localTable p.1 = ghzLocalTable ∧
      statisticalPayoff ghzTable (uniformSettings GHZScenario) p.1 = uniformStrength ghzTable ∧
      statisticalPayoff ghzTable ghzCorrelatedSettings p.1 = correlatedStrength ghzTable := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P80

end

Source

The statistical strength of nonlocality proofs, arXiv:quant-ph/0307125v2, PDF p. 8, Appendix III-F: optimal GHZ setting laws and exact strengths

Read-back

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

Consider three parties, each with settings and outcomes in $\{0,1\}$ . Let $A=\{0,1\}^3$ be the setting space, and let $V$ consist of assignments $v_{ia}\in\{0,1\}$ for every party $i\in\{0,1,2\}$ and setting $a\in\{0,1\}$ . Denote the probability simplices on these spaces by $\Delta_A,\Delta_V$ , and let $\mathcal U\subseteq\Delta_A$ consist of distributions factoring into three single-party setting distributions. A setting $a$ is constrained when $a_0+a_1+a_2$ is $0$ or $2$ ; an outcome $x$ is allowed when $(x_0+x_1+x_2)\bmod2$ is $1$ if $a=(0,0,0)$ and is $0$ otherwise. Define $Q(a,x)$ to be $1/4$ for allowed outcomes at constrained settings, $0$ for other outcomes at constrained settings, and $1/8$ at unconstrained settings. Define $R(a,x)$ to be $3/16$ for allowed outcomes at constrained settings, $1/16$ for other outcomes at constrained settings, and $1/8$ at unconstrained settings. Put $u(a)=1/8$ and let $s_*(a)=1/4$ at constrained settings and $0$ otherwise. For $p\in\Delta_V$ , set $L_p(a,x)=\sum_{v:\,\forall i,\ v_{i,a_i}=x_i}p(v)$ . Define $K(s,p)$ using the joint functions $q(a,x)=s(a)Q(a,x)$ and $r(a,x)=s(a)L_p(a,x)$ : it is $+\infty$ if some $q(a,x)>0$ has $r(a,x)=0$ , and otherwise it is the nonnegative part of $\sum_{a,x}q(a,x)\log_2(q(a,x)/r(a,x))$ , with every summand having $q(a,x)=0$ replaced by $0$ . All these values lie in $[0,+\infty]$ . Set $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 $s_*\in\Delta_A$ , that $u$ factors as $u(a)=\prod_{i=0}^2u_i(a_i)$ for some probability vectors $u_i$ on $\{0,1\}$ , and that

F=U,\qquad U=\max\{0,\tfrac12\log_2(4/3)\},\qquad \inf_{p\in\Delta_V}K(s_*,p)=C,\qquad C=\max\{0,\log_2(4/3)\}.

It also asserts the existence of $p\in\Delta_V$ such that $L_p=R$ , $K(u,p)=F$ , and $K(s_*,p)=C$ .

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