Observation 2: hierarchy with MI and CMI

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.information_hierarchy

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.

Write $\widehat I(A:B)$ and $\widehat I(A:B\mid E)$ for squashing classical mutual information and conditional mutual information, respectively, on the same complete extension and in the same max-then-inf order. Then both comparisons hold:

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

Each is an upper bound on the source-defined squashed intrinsic information.

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 2, (311),(312): both hierarchy comparisons. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem information_hierarchy {p : Box X Y A B} (c : CompleteExtension p) :
    squashedNonlocality c ≤ squashedMI c ∧ squashedNonlocality 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 2 / equations (311), (312)

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 M(c)\qquad\text{and}\qquad N(c)\le C(c).

Here $c$ 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$ . Each positive-weight support consists of vertices and has no proper subset supporting another finite valid decomposition; every such minimal vertex decomposition has exactly one index $z$ with the same total mass at every box. For probability weights $d_z$ , put $r_d^{xy}(a,b,e)=\sum_zd_zw_{ze}v_e(x,y,a,b)$ . With $H(r)=-\sum_ir_i\log_2r_i$ , define

\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}

All subscripts denote marginals obtained by summation, and $j$ ranges over a finite set of size $\ell$ .

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