Unnumbered equation (218): ensemble convex-roof form

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.ensemble_equivalence

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 $\{p_i,P_i\}$ range over all finite ensembles of non-signaling devices in the same polytope, with nonnegative normalized weights and $\sum_i p_iP_i(a,b\mid x,y)=P(a,b\mid x,y)$ for every input and output. Then

N_{\rm sq}(P)=\max_{x,y}\inf_{\{p_i,P_i\}}\sum_i p_i I(A:B)_{P_i(\cdot\mid x,y)}.

The ensemble members need not be extreme, and the infimum precedes the final honest-input maximum.

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, (218): all-device ensemble convex-roof form; no inf/max exchange. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem ensemble_equivalence {p : Box X Y A B} (c : CompleteExtension p) :
    squashedNonlocality c = ensembleForm 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. 45, Equation (218)

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(x,y,a,b)$ , and a complete extension $c$ of $p$ , the theorem asserts

\max_{x,y}\inf_{\substack{d_z\ge0\\\sum_zd_z=1}} I_\downarrow\!\left((a,b,e)\mapsto \sum_zd_zw_{ze}p_{ze}(x,y,a,b)\right) = \max_{x,y}\inf_{\substack{n\ge1\\p=\sum_{i<n}w_ip_i}} \sum_{i<n}w_i I_{p_i(x,y,\cdot,\cdot)}(A:B).

A valid box has nonnegative entries summing to $1$ over both outputs at every input pair, with either party’s marginal independent of the other party’s input. The ensembles on the right range over all finite convex decompositions into valid boxes, allowing zero weights. For a finite law $r$ , $H(r)=-\sum_ur(u)\log_2r(u)$ , $I_r(A:B)=H(r_A)+H(r_B)-H(r)$ , and $I_r(A:B\mid E)=H(r_{AE})+H(r_{BE})-H(r_E)-H(r)$ ; $I_\downarrow(r)$ is the infimum of the latter quantity after every stochastic kernel from $E$ to an arbitrary positive finite set. The data of $c$ are positive integers $Z,E$ and, for each $z<Z$ , a minimal ensemble $(w_{ze},p_{ze})_{e<E}$ of $p$ , with member labels $p_{ze}$ fixed across $z$ . Minimality means that every positive-weight member is extreme among valid boxes and that no ensemble of $p$ has support properly contained in its positive-weight support; extremality rules out any nontrivial convex decomposition into distinct valid boxes. Every minimal ensemble of $p$ , of any finite size, must agree in total weight at every box with exactly one of the indexed ensembles of $c$ .

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