Proposition 8: support-sensitive subextensivity

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.nonlocality_subextensive

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.

Let $d_A=\max_x|\{a:P_A(a\mid x)>0\}|$ and $d_B=\max_y|\{b:P_B(b\mid y)>0\}|$ be the maximum support sizes of the computed no-signaling marginals. Then

N_{\rm sq}(P)\le\log_2\min\{d_A,d_B\}.

Both support sizes are at least one. Reference inputs used to compute the marginals are arbitrary and do not affect their values.

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.52, Proposition 8, (293): support dimensions, not ambient cardinalities.
Normalization and nonempty inputs imply both log arguments are at least one. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem nonlocality_subextensive {p : Box X Y A B} (c : CompleteExtension p) (x : X) (y : Y) :
    squashedNonlocality c ≤ Real.logb 2 (min (aliceSupport p y) (bobSupport p x) : ℕ) := 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. 52, Proposition 8 / equation (293)

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$ , any complete extension $c$ of $p$ , and every specified pair $x\in X,y\in Y$ , the assertion is

N(c)\le \log_2\!\left( \min\left\{ \max_{x'\in X}\left|\left\{a:\sum_bp(x',y,a,b)>0\right\}\right|, \max_{y'\in Y}\left|\left\{b:\sum_ap(x,y',a,b)>0\right\}\right| \right\}\right).

A complete extension consists of positive finite indices $z,e$ , common nonnegative normalized no-signaling boxes $v_e$ , and probability weights $w_{ze}$ reconstructing $p$ for every $z$ . Its positive-weight supports consist of vertices, have no proper subset supporting another finite valid decomposition, and uniquely enumerate all such minimal vertex decompositions by their mass at every box. The quantity on the left is

N(c)=\max_{u,v}\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(u,v,a,b)K(e,j),

where $j<\ell$ , subscripts denote marginals, and $H(r)=-\sum_ir_i\log_2r_i$ . Both support counts use strict positivity; the logarithm is applied to their minimum after conversion to a real number.

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