Unnumbered result (23), (E1): Snl equals Sc

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.nonlocality_equals_correlated_strength

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

prove2quantum

All Bell scenarios have independent finite, nonempty Alice and Bob input and output alphabets. A behavior is a nonnegative conditional output law normalized at every input pair; $\mathrm{NS}$ imposes both no-signaling marginal identities. Processing uses one initial box with rules and randomness fixed independently of the supplied behavior. Write $D(P\Vert Q)$ for classical Kullback–Leibler divergence with natural logarithms, zero numerator contributing zero and positive numerator over zero contributing $+\infty$ . Define $S_b(P\Vert Q)=\max_{x,y}D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ . For an input law $d$ , put $D_d(P\Vert Q)=\sum_{x,y}d(x,y)D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ , with zero-weight terms equal to zero. Let $\mathcal L$ be all local-hidden-variable behaviors on the same alphabets. Define $S_{\rm nl}(P)=\min_{Q\in\mathcal L}S_b(P\Vert Q)$ , $S_u(P)=\min_{Q\in\mathcal L}D_u(P\Vert Q)$ for the uniform joint law $u$ , $S_{uc}(P)=\max_{d_X,d_Y}\min_{Q\in\mathcal L}D_{d_Xd_Y}(P\Vert Q)$ , and $S_c(P)=\max_d\min_{Q\in\mathcal L}D_d(P\Vert Q)$ over all joint laws. For every no-signaling behavior $P$ ,

S_{\rm nl}(P)=S_c(P).

All four strengths are finite. The local minimum defining $S_{\rm nl}$ , every fixed-input-law local minimum, the uniform-input local minimum, and the outer maxima defining $S_{uc}$ and $S_c$ are attained. The identity uses all joint input laws and extends to local boxes, where both sides vanish. This is the equality credited to van Dam, Grunwald and Gill [24] and explicitly reproved in Appendix E.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P29

Formal statement

noncomputable section

open scoped BigOperators ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P29

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Advance50.P47
  (Box IsCorrelation IsNoSignaling HasLocalModel TwoLocalBoxes losrTransform
   correlationMixture)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Dependency50.P47 (Law)

/-- PDF p.8, (23), and p.13, Appendix E, (E1), credited there to [24].
The source's minima/maxima are explicitly attained and finite. The identity uses
all joint input laws; product-law maximum and local minimum are never swapped.
The same formulas include the zero local case. -/
theorem nonlocality_equals_correlated_strength {s : BellScenario} (p : Behavior s)
    (hp : IsNS p) : OptimaAttained p ∧ snl p = correlatedInputStrength p := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 8, Equation (23); Appendix E (E1)

Read-back

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

Let $s$ be any Bell scenario with finite nonempty question sets $X,Y$ and answer sets $A,B$ , and let $p$ be nonnegative and normalized over answers at every question pair, with Bob’s marginal independent of Alice’s question and Alice’s marginal independent of Bob’s question. Let $\mathcal L_s$ be the set of nonnegative normalized arrays $\ell(x,y,a,b)=\sum_h\pi(h)A_h(a\mid x)B_h(b\mid y)$ , with an arbitrary hidden-variable set, a discrete probability mass function $\pi$ , and normalized nonnegative response distributions. Define $D(r\|v)=+\infty$ if some coordinate has $r_i>0$ and $v_i=0$ , and otherwise $D(r\|v)=\max\{0,\sum_i r_i\log(r_i/v_i)\}$ , using natural logarithms and total real division and logarithm at zero. Write

B(p,\ell)=\sup_{x,y}D(p_{xy}\|\ell_{xy}),\qquad W_d(p,\ell)=\sum_{x,y}d(x,y)D(p_{xy}\|\ell_{xy}),\qquad L_d(p)=\inf_{\ell\in\mathcal L_s}W_d(p,\ell),

where $p_{xy}(a,b)=p(x,y,a,b)$ and zero weights multiply infinite divergences to zero. Put $N(p)=\inf_{\ell\in\mathcal L_s}B(p,\ell)$ , let $u(x,y)=1/(|X||Y|)$ , put $U(p)=L_u(p)$ , put $P(p)=\sup_{d_X,d_Y}L_{d_Xd_Y}(p)$ , with the supremum over all nonnegative normalized distributions on $X$ and $Y$ , and put $C(p)=\sup_dL_d(p)$ , with the supremum over all nonnegative normalized joint distributions on $X\times Y$ . The declaration asserts that $N(p),U(p),P(p),C(p)$ are all different from $+\infty$ ; some $\ell\in\mathcal L_s$ satisfies $B(p,\ell)=N(p)$ ; for every joint input distribution $d$ , some $\ell\in\mathcal L_s$ satisfies $W_d(p,\ell)=L_d(p)$ ; some $\ell\in\mathcal L_s$ satisfies $W_u(p,\ell)=U(p)$ ; some pair of input distributions $d_X,d_Y$ satisfies $L_{d_Xd_Y}(p)=P(p)$ ; some joint input distribution $d$ satisfies $L_d(p)=C(p)$ ; and $N(p)=C(p)$ .

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