Theorem 2 (17): contractivity of Sb under global wirings

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.global_contractivity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

All Bell scenarios have independent finite, nonempty Alice and Bob input and output alphabets. A behavior is a nonnegative conditional output law normalized at every input pair; $\mathrm{NS}$ imposes both no-signaling marginal identities. Processing uses one initial box with rules and randomness fixed independently of the supplied behavior. Write $D(P\Vert Q)$ for classical Kullback–Leibler divergence with natural logarithms, zero numerator contributing zero and positive numerator over zero contributing $+\infty$ . Define $S_b(P\Vert Q)=\max_{x,y}D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ . For every pair $P,Q\in\mathrm{NS}$ with the same alphabets and every global wiring $G$ between arbitrary scenarios,

S_b(G(P)\Vert G(Q))\le S_b(P\Vert Q).

The input and output processing kernels of $G$ are arbitrary normalized kernels. Its output behaviors may be signaling. This is data processing for the maximized conditional-output divergence.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P29

Formal statement

noncomputable section

open scoped BigOperators ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P29

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Advance50.P47
  (Box IsCorrelation IsNoSignaling HasLocalModel TwoLocalBoxes losrTransform
   correlationMixture)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Dependency50.P47 (Law)

/-- PDF p.5, Theorem 2, (17), proved on pp.11–12. The two input boxes are NS;
GW output boxes are allowed to be signaling. -/
theorem global_contractivity {s t : BellScenario} (g : GlobalWiring s t)
    (p q : Behavior s) (hp : IsNS p) (hq : IsNS q) :
    sb (g.apply p) (g.apply q) ≤ sb p q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 5, Theorem 2 (17)

Read-back

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

For any scenarios $s,t$ , any nonnegative probability kernels $I(x,y\mid\chi,\psi)$ on source input pairs and $O(\alpha,\beta\mid a,b,x,y,\chi,\psi)$ on target output pairs, and any nonsignaling source correlations $p,q$ , define

G(r)_{\chi\psi}^{\alpha\beta} =\sum_{a,b,x,y} O(\alpha,\beta\mid a,b,x,y,\chi,\psi)\,r_{xy}^{ab}\,I(x,y\mid\chi,\psi).

Then $S(G(p),G(q))\le S(p,q)$ . Every scenario has positive integer input and output sizes; nonsignaling means nonnegative entries, $\sum_{a,b}p_{xy}^{ab}=1$ , Bob’s marginal independent of $x$ , and Alice’s marginal independent of $y$ , and likewise for $q$ . The kernels are normalized for every choice of their conditioning arguments, with no locality requirement. For any real arrays $r,u$ , $S(r,u)=\sup_{x,y}D(r_{xy}\Vert u_{xy})$ , where $D(P\Vert Q)=\infty$ if some $P_i>0$ has $Q_i=0$ , and otherwise $D(P\Vert Q)=\max\{0,\sum_iP_i\log(P_i/Q_i)\}$ , interpreted in $[0,\infty]$ , using natural logarithms and the total conventions $a/0=0$ , $\log0=0$ .

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