Theorem 10: product-input statistical strength is a Bell monotone

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.product_strength_bell_monotone

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. A Bell nonlocality monotone is a family of finite, nonnegative values on no-signaling behaviors in all scenarios. It vanishes on every local behavior and does not increase under LOSR or WPICC operations, including operations changing alphabet sizes. The product-input strength is finite, vanishes on local behaviors, and satisfies

S_{uc}(W(P))\le S_{uc}(P)\quad(P\in\mathrm{NS},\ W\in\mathrm{LOSR}\cup\mathrm{WPICC}).

Thus $S_{uc}$ is a Bell nonlocality monotone. The local comparison class is $\mathcal L$ ; the quantum-comparison variant is not covered. WPICC uses Appendix A’s fixed no-preparation LOSR branch and random adaptive preparation branches in which at least one party measures before the final inputs.

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.8, Theorem 10, proved on pp.14–15: (22b), with local comparison boxes.
The quantum-comparison variant of (24) is not asserted to be monotone. -/
theorem product_strength_bell_monotone :
    IsBellMonotone (fun _ 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. 8, Theorem 10

Read-back

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

For every scenario $s$ , whose input and output sets have positive integer sizes, define

C_s(p)= \sup_{\substack{d_X(x)\ge0,\ \sum_xd_X(x)=1\\ d_Y(y)\ge0,\ \sum_yd_Y(y)=1}} \ \inf_{q\ \mathrm{local}} \sum_{x,y}d_X(x)d_Y(y)\,D(p_{xy}\Vert q_{xy}).

The infimum is over nonnegative normalized correlations $q$ admitting $q_{xy}^{ab}=\sum_\lambda\mu(\lambda)A_\lambda(a\mid x)B_\lambda(b\mid y)$ , with probability-vector responses and a probability mass function on an arbitrary type. The divergence is $\infty$ if some $P_i>0$ has $Q_i=0$ , and otherwise is $\max\{0,\sum_iP_i\log(P_i/Q_i)\}$ , using natural logarithms, $a/0=0$ , and $\log0=0$ ; weighted sums take place in $[0,\infty]$ , with $0\cdot\infty=0$ . The theorem says that $C_s(p)$ is finite for every nonsignaling correlation, is zero for every local correlation, and satisfies $C_t(w(p))\le C_s(p)$ for every nonsignaling $p$ under both of the following operation classes. The first class is represented on every real array by

w(r)_{\chi\psi}^{\alpha\beta} =\sum_{a,b,x,y} \left(\sum_\lambda\mu(\lambda)O^A_\lambda(\alpha\mid a,x,\chi)O^B_\lambda(\beta\mid b,y,\psi)\right) r_{xy}^{ab} \left(\sum_\eta\nu(\eta)I^A_\eta(x\mid\chi)I^B_\eta(y\mid\psi)\right),

where all kernels are probability vectors and the input and output mixtures use separate probability mass functions on arbitrary types. The second class agrees on every nonsignaling correlation with a probability mixture of deterministic preparations that separately choose the two inputs from the respective target inputs and locally process the outcomes; or first fix Alice’s input and, depending on her outcome, either choose Bob’s input from his target input while Alice’s output ignores Bob’s outcome, or fix Bob’s input while both outputs may depend on Bob’s outcome; or use the symmetric Bob-first construction. Each final output depends on its own target input and the specified available outcomes, and deterministic transformations sum source entries with output indicators. Nonsignaling correlations are nonnegative, normalized over outputs for each input pair, and have each party’s marginal independent of the other party’s input; operations in the second class are unrestricted on other arrays.

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