Proposition 6: GMDLOPC monotonicity for the explicit source map

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.generalized_monotonicity

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 $\mu$ on $L$ and $\nu$ on $M$ be independent shared probability laws on finite nonempty alphabets. Let $D_A(x\mid x_o,l)$ , $D_B(y\mid y_o,l)$ , $R_A(a_o\mid a,x,m)$ and $R_B(b_o\mid b,y,m)$ be normalized local stochastic kernels. Define the source map

P_o(a_o,b_o\mid x_o,y_o)=\sum_{l,m,x,y,a,b}\mu(l)\nu(m)D_A(x\mid x_o,l)D_B(y\mid y_o,l)P(a,b\mid x,y)R_A(a_o\mid a,x,m)R_B(b_o\mid b,y,m).

Then

N_{\rm sq}(P_o)\le N_{\rm sq}(P).

This states monotonicity for the displayed source class of maps.

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)

/-- PDF pp.48–49, Proposition 6, (240): monotonicity for the explicit map.
The apparent max/inf exchange in (260)–(261) is a moderation concern, not a premise. Source convention: Eve keeps the dice
result (p.22, XI.B.3); CE members may depend on (z,e) -/
theorem generalized_monotonicity {X Y A B Xo Yo Ao Bo L M : Type}
    [Fintype X] [Fintype Y] [Fintype A] [Fintype B]
    [Fintype Xo] [Fintype Yo] [Fintype Ao] [Fintype Bo] [Fintype L] [Fintype M]
    [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B]
    [Nonempty Xo] [Nonempty Yo] [Nonempty Ao] [Nonempty Bo] [Nonempty L] [Nonempty M]
    (g : GeneralLocalMap X Y A B Xo Yo Ao Bo L M) (p : Box X Y A B)
    (cp : CompleteExtension p) (co : CompleteExtension (g.apply p)) :
    squashedNonlocality co ≤ squashedNonlocality cp := by sorry

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. 48, Proposition 6 / equations (240)–(245)

Read-back

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

For arbitrary finite nonempty sets $X,Y,A,B,X_o,Y_o,A_o,B_o,L,M$ , let $g$ consist of nonnegative normalized laws $\mu(l),\nu(m)$ , input kernels $\alpha(l,x_o,x),\beta(l,y_o,y)$ normalized over $x,y$ , and output kernels $\gamma(m,a,x,a_o),\delta(m,b,y,b_o)$ normalized over $a_o,b_o$ , for every conditioning index. Let $p$ be a real-valued box, and define

q(x_o,y_o,a_o,b_o)= \sum_{l,m,x,y,a,b} \mu(l)\nu(m)\alpha(l,x_o,x)\beta(l,y_o,y) p(x,y,a,b)\gamma(m,a,x,a_o)\delta(m,b,y,b_o).

For every complete extension $c_p$ of $p$ and complete extension $c_o$ of $q$ , the theorem asserts $N(c_o)\le N(c_p)$ . A valid box has nonnegative normalized output laws and marginals independent of the other party’s input. A complete extension of a box consists of positive finite input and label counts and a minimal convex ensemble of that box at each extension input, with fixed member labels across inputs; every minimal ensemble, of any finite size, agrees in total weight at each box with exactly one indexed ensemble. An ensemble is minimal when its positive-weight members are extreme valid boxes and no ensemble of the same box has properly contained support; extremality excludes nontrivial convex decompositions into distinct valid boxes. For an extension $c$ with ensembles $(w_{ze},p_{ze})$ , its quantity is

N(c)=\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),

using the input and output alphabets of its underlying box. Here $I_\downarrow(r)$ is the infimum, over stochastic kernels from $e$ to any positive finite output set, of $H(AJ)+H(BJ)-H(J)-H(ABJ)$ for the resulting law, where $H(s)=-\sum_us(u)\log_2s(u)$ . All laws may contain zero weights, and their normalization requirements apply at every conditioning index.

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