Unnumbered equation (216): optimization over unary-input extensions

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.unary_extension_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 $\widetilde P(a,b,e\mid x,y)$ range over all finite-output, fully tripartite non-signaling extensions of $P$ with unary Eve input. The extension constraints include input-independent Eve marginal and the no-signaling equalities conditional on each Eve output. Then

N_{\rm sq}(P)=\max_{x,y}\inf_{\widetilde P:\,\sum_e\widetilde P=P} I(A:B\mid E)_{\widetilde P(\cdot\mid x,y)}.

No minimizing extension is assumed to exist, and the CE generation property is not built into the definition of complete extension.

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 pp.44–45, (216): CE squashing equals optimization over all unary extensions.
The cited generation result remains theorem content, never a CE field. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem unary_extension_equivalence {p : Box X Y A B} (c : CompleteExtension p) :
    squashedNonlocality c = extensionForm 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. 44, Equation (216)

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 following two real quantities are equal. A valid box has nonnegative entries, total output mass $1$ at every input pair, and each party’s output marginal independent of the other party’s input. A finite ensemble reconstructs $p$ as a convex combination of valid boxes; its support consists of its positively weighted members. Such an ensemble is minimal when those members are extreme valid boxes and no ensemble reconstructing $p$ has properly smaller support by inclusion; extremality means that a convex decomposition with coefficient in $(0,1)$ forces both component boxes to equal the original box. The complete extension $c$ consists of positive finite numbers $Z,E$ and minimal ensembles $(w_{ze},p_{ze})_{e<E}$ , with common member labels across $z$ , such that every minimal ensemble of $p$ , of any finite size, has the same mass at each box as exactly one indexed ensemble. Put $H(q)=-\sum_uq(u)\log_2q(u)$ and $I_r(A:B\mid E)=H(r_{AE})+H(r_{BE})-H(r_E)-H(r)$ ; let $I_\downarrow(r)$ be the infimum of this conditional mutual information after any stochastic kernel from $E$ to any positive finite output set. The asserted equality is

\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\\D\text{ as below}}} I_{D(x,y,\cdot,\cdot,\cdot)}(A:B\mid E).

Here $D(x,y,a,b,e)$ , with $e<n$ , must be nonnegative, satisfy $\sum_eD(x,y,a,b,e)=p(x,y,a,b)$ , have $\sum_{a,b}D(x,y,a,b,e)$ independent of both $x,y$ , have $\sum_aD(x,y,a,b,e)$ independent of $x$ , and have $\sum_bD(x,y,a,b,e)$ independent of $y$ . Neither infimum is restricted to strictly positive weights or entries.

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