Corollary 5: convexification bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.convexification_bound

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 every device $R$ , let $U(R)$ be the smaller of its squashed MI and squashed CMI values, each computed on a complete extension. The lower convex hull is the infimum of $\sum_i p_i U(P_i)$ over all finite normalized ensembles with $\sum_i p_iP_i=P$ at every device input. Complete extensions of the constituent devices are included as representation data. Then

N_{\rm sq}(P)\le\operatorname{LCH}\{\widehat I(A:B),\widehat I(A:B\mid E)\}(P).

The score set is nonempty by the one-term decomposition and bounded below by zero; it is a hull over entire feasible device mixtures, not sampled interpolation.

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.55, Corollary 5, (317): the actual lower convex hull bounds Nsq. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem convexification_bound {p : Box X Y A B} (c : CompleteExtension p) :
    squashedNonlocality c ≤ squashedLowerHull p := 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. 55, Corollary 5 / equation (317)

Read-back

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

For finite nonempty sets $X,Y,A,B$ , a box $p$ , and a complete extension $c$ of $p$ , the theorem asserts

N(c)\le \inf_{\substack{n\ge1,\ p=\sum_{i<n}w_ip_i\\ c_i\text{ a complete extension of }p_i}} \sum_{i<n}w_i\min\{S_{\mathrm{MI}}(c_i),S_{\mathrm{CMI}}(c_i)\}.

Here every ensemble uses nonnegative weights summing to $1$ and valid member boxes, meaning normalized nonnegative output laws whose individual marginals are independent of the other party’s input. A complete extension has positive finite numbers of inputs and labels, with a minimal ensemble at each extension input and fixed member labels across those inputs; every minimal ensemble of the underlying box, of any finite size, agrees in total weight at every box with exactly one indexed ensemble. Minimality requires extreme positive-weight members and excludes any ensemble with properly contained support; extremality means that a convex decomposition with coefficient strictly between $0$ and $1$ forces both components to equal the box. For any such extension $h$ , with ensembles $(w_{ze},q_{ze})$ , set $r^{x,y,d}(a,b,e)=\sum_zd_zw_{ze}q_{ze}(x,y,a,b)$ , where $d$ ranges over all probability laws on its extension inputs. Then

N(h)=\max_{x,y}\inf_d I_\downarrow(r^{x,y,d}),\quad S_{\mathrm{MI}}(h)=\max_{x,y}\inf_d I(r^{x,y,d}_{AB}),\quad S_{\mathrm{CMI}}(h)=\max_{x,y}\inf_d I(A:B\mid E)_{r^{x,y,d}}.

With $H(q)=-\sum_uq(u)\log_2q(u)$ , the information expressions are $I(A:B)=H(A)+H(B)-H(AB)$ and $I(A:B\mid E)=H(AE)+H(BE)-H(E)-H(ABE)$ ; $I_\downarrow$ takes the infimum of conditional mutual information after any stochastic kernel on $E$ with a positive finite output count. Zero weights are permitted throughout, and every $c_i$ , including one attached to a zero-weight member, must exist.

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