Theorem 8: Bell monotonicity of the relative entropy of nonlocality

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.relative_entropy_nonlocality_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 relative entropy of nonlocality satisfies

S_{\rm nl}(P)=0\quad(P\in\mathcal L),\qquad S_{\rm nl}(W(P))\le S_{\rm nl}(P)\quad(P\in\mathrm{NS},\ W\in\mathrm{LOSR}\cup\mathrm{WPICC}).

The values are finite and nonnegative. This supplies a nonlocality measure compatible with both free-operation classes. 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.7, Theorem 8, with Definitions 5 and 7 expanded by the predicates.
Includes vanishing on all local boxes and monotonicity across scenarios. -/
theorem relative_entropy_nonlocality_bell_monotone :
    IsBellMonotone (fun _ p => snl 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. 7, Theorem 8

Read-back

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

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

N_s(p)=\inf_{q\ \mathrm{local}}\ \sup_{x,y}D(p_{xy}\Vert q_{xy}),

where a local $q$ is nonnegative and normalized at each input pair and admits $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. Here $D(P\Vert Q)$ is $\infty$ if some $P_i>0$ has $Q_i=0$ , and otherwise is $\max\{0,\sum_iP_i\log(P_i/Q_i)\}$ ; logarithms are natural, $a/0=0$ , and $\log0=0$ . This quantity is finite on every nonsignaling correlation and zero on every local correlation, and $N_t(w(p))\le N_s(p)$ for every nonsignaling $p$ under either of two classes of operations. The first class consists of operations represented on all real arrays 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 every kernel is a probability vector and the two mixing laws are separate. The second class consists of operations agreeing on every nonsignaling correlation with a probability mixture of deterministic preparations: separately choose the source inputs from the target inputs and process each local outcome; or fix Alice’s input first 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. Final outputs depend on their own target inputs and the stated outcomes, and deterministic transformations sum source entries with output indicators. Mixing types may be infinite. Nonsignaling here includes nonnegativity, output normalization, and independence of each marginal from the other party’s input; the second operation class is unrestricted elsewhere.

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