Lemma 12 (G2): UCLOSR monotonicity of Suc

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.uncorrelated_product_strength_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 an input law $d$ , put $D_d(P\Vert Q)=\sum_{x,y}d(x,y)D(P(\cdot,\cdot\mid x,y)\Vert Q(\cdot,\cdot\mid x,y))$ , with zero-weight terms equal to zero. Let $\mathcal L$ be all local-hidden-variable behaviors on the same alphabets. Define $S_{\rm nl}(P)=\min_{Q\in\mathcal L}S_b(P\Vert Q)$ , $S_u(P)=\min_{Q\in\mathcal L}D_u(P\Vert Q)$ for the uniform joint law $u$ , $S_{uc}(P)=\max_{d_X,d_Y}\min_{Q\in\mathcal L}D_{d_Xd_Y}(P\Vert Q)$ , and $S_c(P)=\max_d\min_{Q\in\mathcal L}D_d(P\Vert Q)$ over all joint laws. For every no-signaling behavior $P$ and every UCLOSR wiring $U$ , whose input and output kernels are products of four normalized one-party kernels,

S_{uc}(U(P))\le S_{uc}(P).

The component wiring itself has no shared hidden variable. This is the uncorrelated component monotonicity used in the LOSR decomposition.

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.15, Lemma 12, (G2): four independent local kernels, with arbitrary
initial and final finite nonempty alphabets. -/
theorem uncorrelated_product_strength_contractivity {s t : BellScenario}
    (u : UncorrelatedWiring s t) (p : Behavior s) (hp : IsNS p) :
    suc (u.apply p) ≤ suc p := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 15, Lemma 12 (G2)

Read-back

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

Let $s,t$ be any Bell scenarios, each with finite nonempty question and answer sets, denoted $X,Y,A,B$ for $s$ and $X',Y',A',B'$ for $t$ . Choose nonnegative normalized kernels $I_A(x\mid\chi)$ , $I_B(y\mid\psi)$ , $O_A(\alpha\mid a,x,\chi)$ , and $O_B(\beta\mid b,y,\psi)$ , and define the transformation

(ur)(\chi,\psi,\alpha,\beta)= \sum_{a,b,x,y}O_A(\alpha\mid a,x,\chi)O_B(\beta\mid b,y,\psi)\, r(x,y,a,b)I_A(x\mid\chi)I_B(y\mid\psi).

Let $p$ be a nonnegative normalized source array whose Bob marginal is independent of Alice’s question and whose Alice marginal is independent of Bob’s question. For either scenario, let $\mathcal L$ consist of all nonnegative normalized arrays $\ell(x,y,a,b)=\sum_h\pi(h)A_h(a\mid x)B_h(b\mid y)$ , with an arbitrary hidden-variable set, a discrete probability mass function $\pi$ , and nonnegative normalized response distributions $A_h,B_h$ . Define $D(r\|v)=+\infty$ when some $r_i>0$ has $v_i=0$ , and otherwise $D(r\|v)=\max\{0,\sum_i r_i\log(r_i/v_i)\}$ in $[0,+\infty]$ , using natural logarithms and total real division and logarithm at zero. Define the product-input strength by

S_{\mathrm{prod}}(r)= \sup_{\substack{d_X\ge0,\ \sum_xd_X(x)=1\\d_Y\ge0,\ \sum_yd_Y(y)=1}} \inf_{\ell\in\mathcal L} \sum_{x,y}d_X(x)d_Y(y)\, D\bigl(r(x,y,\cdot,\cdot)\,\|\,\ell(x,y,\cdot,\cdot)\bigr).

Then $S_{\mathrm{prod}}(up)\le S_{\mathrm{prod}}(p)$ , with each strength evaluated in its corresponding scenario. Input distributions may have zero entries, and weighted divergences use $0\cdot(+\infty)=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