Observation 3: minimum of two upper bounds

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.information_minimum

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.

With $\widehat I(A:B)$ and $\widehat I(A:B\mid E)$ denoting the two squashed information functions on the complete extension,

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

This combines both individual hierarchy bounds.

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.54, Observation 3, (313): the minimum of the two squashed bounds. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem information_minimum {p : Box X Y A B} (c : CompleteExtension p) :
    squashedNonlocality c ≤ min (squashedMI c) (squashedCMI 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. 54, Observation 3 / equation (313)

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$ , and any complete extension $c$ of $p$ , the assertion is

N(c)\le\min\{M(c),C(c)\}.

A complete extension supplies positive finite indices $z,e$ , common nonnegative normalized no-signaling boxes $v_e$ , and probability weights $w_{ze}$ reconstructing $p$ for each $z$ . Every positive-weight support consists of vertices and has no proper subset supporting another finite valid decomposition, and every such minimal vertex decomposition corresponds to exactly one $z$ , with equality of total mass at every box. For probability weights $d_z$ , let $r_d^{xy}(a,b,e)=\sum_zd_zw_{ze}v_e(x,y,a,b)$ . Writing $H(r)=-\sum_ir_i\log_2r_i$ , the three real quantities are

\begin{aligned} M(c)&=\max_{x,y}\inf_d \bigl[H((r_d^{xy})_A)+H((r_d^{xy})_B)-H((r_d^{xy})_{AB})\bigr],\\ C(c)&=\max_{x,y}\inf_d \bigl[H((r_d^{xy})_{AE})+H((r_d^{xy})_{BE})-H((r_d^{xy})_E)-H(r_d^{xy})\bigr],\\ N(c)&=\max_{x,y}\inf_d\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_er_d^{xy}(a,b,e)K(e,j). \end{aligned}

Subscripts mean summing out omitted coordinates, $j<\ell$ , and all probability weights may include zeros.

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