Proposition 4: convexity

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.nonlocality_convex

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.

For two devices $P,Q$ in the same fixed polytope and every $\lambda\in[0,1]$ , with the mixture computed pointwise,

N_{\rm sq}(\lambda P+(1-\lambda)Q)\le\lambda N_{\rm sq}(P)+(1-\lambda)N_{\rm sq}(Q).

The claim holds for arbitrary complete extensions of each indicated device and includes both endpoints.

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.46, Proposition 4, (222): convexity, including both endpoints.
The CE arguments are arbitrary complete extensions of the specified devices. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem nonlocality_convex (p q : Box X Y A B) (t : ℝ) (ht : 0 ≤ t) (htOne : t ≤ 1)
    (cp : CompleteExtension p) (cq : CompleteExtension q)
    (cm : CompleteExtension (correlationMixture p q t)) :
    squashedNonlocality cm ≤ t * squashedNonlocality cp + (1-t) * squashedNonlocality cq := 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. 46, Proposition 4 / equation (222)

Read-back

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

For finite nonempty alphabets $X,Y,A,B$ , any real arrays $p,q$ , any real $t$ with $0\le t\le1$ , and any complete extensions $c_p,c_q,c_m$ of $p,q,m$ , respectively, where $m(x,y,a,b)=t\,p(x,y,a,b)+(1-t)q(x,y,a,b)$ , the assertion is

N(c_m)\le t\,N(c_p)+(1-t)N(c_q).

Here a complete extension $c$ supplies positive finite indices $z,e$ , probability weights $w_{ze}$ , and common nonnegative normalized no-signaling boxes $v_e$ reconstructing its box for every $z$ . Every positive-weight support consists of vertices and has no proper subset supporting another finite valid decomposition, and every such minimal vertex decomposition has a unique $z$ with the same total weight at every box. For each such extension,

N(c)=\max_{x,y}\inf_{\substack{d_z\ge0\\\sum_zd_z=1}} \inf_{\substack{\ell>0\\K(e,j)\ge0,\ \sum_jK(e,j)=1}} \bigl[H(s_{AJ})+H(s_{BJ})-H(s_J)-H(s)\bigr], \quad s(a,b,j)=\sum_{z,e}d_zw_{ze}v_e(x,y,a,b)K(e,j),

with $j<\ell$ , marginals formed by summation, and $H(r)=-\sum_ir_i\log_2r_i$ . The endpoints $t=0$ and $t=1$ are included, and the three complete extensions are quantified independently.

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