Unnumbered equation (3): equivalence to the AMP ensemble optimization

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.amp_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.

For a fixed honest input $(x,y)$ , define $I_{\rm AMP,(x,y)}(P)$ as the infimum of $I(A:B\downarrow E)$ of the measured ensemble law $p(e)P^e(a,b\mid x,y)$ over every finite non-signaling ensemble that reconstructs $P$ at every input. Then

\max_{x,y}I_{\rm AMP,(x,y)}(P)=N_{\rm sq}(P).

The ensemble constraints remain global even though information is evaluated at a fixed honest setting.

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.3,45, (3): equality with the AMP ensemble optimization. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem amp_equivalence {p : Box X Y A B} (c : CompleteExtension p) :
    finiteMax (fun xy : X × Y => ampAtInput p xy.1 xy.2) = squashedNonlocality c := 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 (3) / Appendix XVI A

Read-back

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

For finite nonempty input and output sets $X,Y,A,B$ , let $p:X\times Y\times A\times B\to\mathbb R$ , and let $c$ be a complete extension of $p$ . Here a valid box has nonnegative entries summing to $1$ over $a,b$ for every $x,y$ , with $\sum_a p(x,y,a,b)$ independent of $x$ and $\sum_b p(x,y,a,b)$ independent of $y$ . A finite ensemble of $p$ consists of valid boxes $p_i$ and nonnegative weights $w_i$ summing to $1$ , with $p=\sum_iw_ip_i$ . Its support consists of the boxes occurring with positive weight; it is minimal when every positively weighted member is an extreme point of the valid boxes and no ensemble of $p$ has support properly contained in its support. An extreme point is a valid box that cannot be expressed as a convex mixture with coefficient strictly between $0$ and $1$ of two valid boxes unless both equal it. The extension $c$ supplies positive integers $Z,E$ and a minimal ensemble $(w_{ze},p_{ze})_{e<E}$ for every $z<Z$ , with $p_{ze}$ independent of $z$ ; every minimal ensemble of $p$ , of any finite size, has the same total weight at each box as exactly one of these ensembles. For a finite joint law $r(a,b,e)$ , write

I_r(A:B\mid E)=H(r_{AE})+H(r_{BE})-H(r_E)-H(r), \qquad H(q)=-\sum_u q(u)\log_2q(u),

and define $I_\downarrow(r)$ as the infimum of $I(A:B\mid J)$ after applying any stochastic kernel $e\mapsto j$ with an arbitrary positive finite number of outputs, so that the resulting law is $\sum_e r(a,b,e)K(e,j)$ . The theorem asserts

\max_{x,y}\ \inf_{\substack{n\ge1\\p=\sum_{i<n}w_ip_i}} I_\downarrow\!\bigl((a,b,i)\mapsto w_ip_i(x,y,a,b)\bigr) = \max_{x,y}\ \inf_{\substack{d_z\ge0\\\sum_{z<Z}d_z=1}} I_\downarrow\!\left((a,b,e)\mapsto \sum_{z<Z}d_zw_{ze}p_{ze}(x,y,a,b)\right).

The ensemble infimum on the left ranges over all finite ensembles, without a minimality requirement, and permits zero weights.

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