Proposition 3: nonnegativity and vanishing on local boxes

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.nonlocality_nonnegative_local

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

prove2quantum

All input and output alphabets are finite and nonempty. Let $P(a,b\mid x,y)$ be a normalized nonnegative bipartite non-signaling device, and let $\mathcal E(P)$ be its complete extension, with possibly input-dependent pure-member labels. All Shannon information quantities are in bits, with $0\log_2 0=0$ . Write $N_{\rm sq}(P)$ for the maximum over honest settings $(x,y)$ of the infimum, over Eve's general measurements, of intrinsic information; intrinsic information itself minimizes classical conditional mutual information over arbitrary stochastic channels on Eve.

Then

N_{\rm sq}(P)\ge0,\qquad P\text{ admits a local hidden-variable model}\ \Longrightarrow\ N_{\rm sq}(P)=0.

Vanishing on local devices is one-way and asserts no faithfulness converse.

Eve retains the dice result $z$ and extension output $e$ . Squashed CMI conditions on $(z,e)$ ; intrinsic-information channels may depend on both. This is the operational convention of XI.B.3 used by the proof, rather than discarding the dice result in display (7).

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)

section Devices

variable {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B]
  [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B]

/-- PDF p.45, Proposition 3, (219): nonnegative and zero on local boxes;
no converse, optimizer, or favorable extension is assumed. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem nonlocality_nonnegative_local {p : Box X Y A B} (c : CompleteExtension p) :
    0 ≤ squashedNonlocality c ∧ (HasLocalModel p → squashedNonlocality c = 0) := by sorry

end Devices

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. 45, Proposition 3 / equation (219)

Read-back

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

For finite nonempty alphabets $X,Y,A,B$ , any box $p$ , and any complete extension $c$ of $p$ , the assertion is $0\le N(c)$ , and, if $p$ has a local model, then $N(c)=0$ . A complete extension consists of positive finite index sets $z,e$ , common valid boxes $v_e$ , and probability weights $w_{ze}$ reconstructing $p=\sum_e w_{ze}v_e$ for every $z$ ; valid means nonnegative, normalized at every input, and no-signaling in both directions. Each positive-weight support consists of vertices and has no proper subset supporting any finite valid decomposition of $p$ , and each such minimal vertex decomposition is represented by exactly one $z$ , with equality of total mass at every box. For probability weights $d_z$ , define $r_d^{xy}(a,b,e)=\sum_zd_zw_{ze}v_e(x,y,a,b)$ ; then

N(c)=\max_{x,y}\inf_d\inf_{\substack{m>0\\K(e,j)\ge0,\ \sum_jK(e,j)=1}} \bigl[H(s_{AJ})+H(s_{BJ})-H(s_J)-H(s)\bigr], \qquad s(a,b,j)=\sum_er_d^{xy}(a,b,e)K(e,j),

where $H(r)=-\sum_ir_i\log_2r_i$ . Having a local model means that $p$ is nonnegative and normalized and that there exist a type $L$ , a probability mass function $\mu$ on $L$ , and probability response vectors $\alpha_l(\cdot\mid x)$ , $\beta_l(\cdot\mid y)$ such that $p(x,y,a,b)=\sum'_l\mu(l)\alpha_l(a\mid x)\beta_l(b\mid y)$ ; $L$ is not required to be finite.

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