Unnumbered HRW formula (320) and local fraction

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.hrw_loss_fraction

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

prove2quantum

Let $x,y,a,b\in\{0,1\}$ . For real parameters $\delta,\eta$ , define the binary HRW device as follows. At $x=y=0$ , each equal-output event has probability $(1-\delta)/2$ and each unequal-output event has probability $\delta/2$ . At every other setting, each CHSH-winning event $a\oplus b=xy$ has probability $3/8-\eta/2$ and each losing event has probability $1/8+\eta/2$ . Let $\epsilon(P)$ be the CHSH loss averaged over independent uniform inputs. In the printed single-vertex convention, $C(P)$ is the infimum of $t\in[0,1]$ in decompositions $P=tV+(1-t)L$ with $V$ a nonlocal extreme non-signaling device and $L$ local.

For $0\le\delta\le1$ and $-1/4\le\eta\le3/4$ , the HRW device is valid and non-signaling, and

\epsilon(P)=\frac14\left(\frac34+\delta+3\eta\right).

Within the further sector $\eta\le1/12-\delta/3$ ,

C(P)=\frac14-\delta-3\eta,\qquad P\text{ is nonlocal}\ \Longleftrightarrow\ \epsilon(P)<\frac14.

The feasible sector prevents empty-set infimum defaults; this statement makes no fraction claim for other CHSH sectors.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P22

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P22

attribute [local instance] Classical.propDecidable Classical.decEq

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

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

open QAlgorithms.Papers.Independent.Information100.P27 (shannon)

open QAlgorithms.Papers.Independent.Gap48.P25 (classicalMI)

/-- PDF p.56, (319),(320): validity on the full printed rectangle and the loss
formula. The fraction and local/nonlocal boundary refer only to the indicated
CHSH sector, including its local endpoint. No other relabeling sector is claimed. -/
theorem hrw_loss_fraction (delta eta : ℝ)
    (hd : 0 ≤ delta) (hdOne : delta ≤ 1) (he : -(1/4 : ℝ) ≤ eta) (heUpper : eta ≤ 3/4) :
    ValidDevice (hrwBox delta eta) ∧
    chshLoss (hrwBox delta eta) = (1/4 : ℝ) * (3/4 + delta + 3*eta) ∧
    (eta ≤ 1/12 - delta/3 →
      nonlocalityFraction (hrwBox delta eta) = 1/4 - delta - 3*eta ∧
      (¬ HasLocalModel (hrwBox delta eta) ↔ chshLoss (hrwBox delta eta) < 1/4)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P22

end

Source

Limitations on device independent key secure against non signaling adversary via the squashed non-locality, arXiv:1903.12154v7, PDF p. 56, Equations (319), (320) and following local-fraction formula

Read-back

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

For every pair of real numbers $\delta,\eta$ satisfying $0\le\delta\le1$ and $-\tfrac14\le\eta\le\tfrac34$ , define the Boolean-input, Boolean-output array

p(x,y,a,b)= \begin{cases} (1-\delta)/2,&x=y=0,\ a=b,\\ \delta/2,&x=y=0,\ a\ne b,\\ 3/8-\eta/2,&(x,y)\ne(0,0),\ a\oplus b=xy,\\ 1/8+\eta/2,&(x,y)\ne(0,0),\ a\oplus b\ne xy. \end{cases}

Here all four arguments range over $\{0,1\}$ , identified with the Booleans. The theorem asserts that $p$ is nonnegative, that $\sum_{a,b}p(x,y,a,b)=1$ for every $x,y$ , and that its marginals satisfy $\sum_a p(x,y,a,b)=\sum_a p(x',y,a,b)$ for all $x,x',y,b$ and $\sum_b p(x,y,a,b)=\sum_b p(x,y',a,b)$ for all $y,y',x,a$ . Moreover, writing $\ell(p)=\tfrac14\sum_{x,y,a,b:\,a\oplus b\ne xy}p(x,y,a,b)$ , it asserts

\ell(p)=\frac14\left(\frac34+\delta+3\eta\right).

To specify the remaining conclusions, call an array local if it is nonnegative and normalized at each input pair and there exist an arbitrary type $L$ , a probability mass function $\mu$ on $L$ , and nonnegative response functions $\alpha_l(a\mid x)$ , $\beta_l(b\mid y)$ , each summing to $1$ over its output, such that $p(x,y,a,b)=\sum'_l\mu(l)_{\mathbb R}\alpha_l(a\mid x)\beta_l(b\mid y)$ , where $\mu(l)_{\mathbb R}$ is the real value of the probability mass. Call an array a vertex if it is nonnegative, normalized, and no-signaling as above, and every expression $v=tq+(1-t)r$ with $0<t<1$ and nonnegative, normalized, no-signaling arrays $q,r$ forces $q=v$ and $r=v$ . Define $F(p)$ as the real infimum of all $t\in[0,1]$ for which $p=tv+(1-t)l$ , with $v$ a vertex having no local model and $l$ local; this uses the total real-infimum convention, including value $0$ for an empty admissible set. If additionally $\eta\le\tfrac1{12}-\tfrac{\delta}{3}$ , then

F(p)=\frac14-\delta-3\eta, \qquad p\text{ has no local model}\ \Longleftrightarrow\ \ell(p)<\frac14.

All parameter endpoints are included, and this final implication includes equality in its additional bound on $\eta$ .

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