Theorem 9: uniform-input statistical strength is not a monotone

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.uniform_strength_not_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. There are scenarios, an LOSR wiring $W$ , and $P\in\mathrm{NS}$ such that

S_u(W(P))>S_u(P).

Consequently $S_u$ is neither an LOSR monotone, nor a WPICC monotone, nor a Bell nonlocality monotone. This rules out the uniform-input strength as a free-operation monotone. No quantum-realizability hypothesis or specific factor-four witness is part of this statement. 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 9, and p.13 opening of Appendix F: a strict LOSR increase
exists, hence all three monotone claims fail. No quantum realization is required.
This states no claim about the inconsistent printed factor-four witness (F10). -/
theorem uniform_strength_not_monotone :
    (∃ (s t : BellScenario) (w : BellOperation s t) (p : Behavior s),
      IsLOSR w ∧ IsNS p ∧ su p < su (w p)) ∧
    ¬ IsLOSRMonotone (fun _ p => su p) ∧
    ¬ IsWPICCMonotone (fun _ p => su p) ∧
    ¬ IsBellMonotone (fun _ p => su 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 9

Read-back

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

For a scenario $s$ with positive integer sizes $n_X,n_Y,n_A,n_B$ , define the extended nonnegative quantity

U_s(p)=\inf_{q\ \mathrm{local}} \sum_{x,y}\frac{1}{n_Xn_Y}\,D(p_{xy}\Vert q_{xy}).

A local $q$ is nonnegative, normalized over outputs for each input pair, and has $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 $D(P\Vert Q)=\max\{0,\sum_iP_i\log(P_i/Q_i)\}$ , using natural logarithms, $a/0=0$ , and $\log0=0$ . The theorem asserts all four of the following: there exist scenarios $s,t$ , an operation $w$ , and a nonsignaling correlation $p$ with $U_s(p)<U_t(w(p))$ , where $w$ is represented on every real array by separate local input and output mixtures; the function $U$ fails the corresponding normalized monotonicity predicate; it fails the normalized monotonicity predicate for mixtures of the deterministic preparations described below; and it fails the conjunction of those two predicates. Explicitly, the first operation class has

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),

with probability-vector kernels and arbitrary mixing types. The second class need only agree on nonsignaling correlations with a probability mixture of preparations that separately choose inputs and locally process outcomes, or first fix Alice’s input and, depending on her outcome, either choose Bob’s input from his target input while Alice’s final output ignores Bob’s outcome, or fix Bob’s input and allow both final outputs to depend on Bob’s outcome, or use the symmetric Bob-first construction. Final outputs depend on their own target inputs and the specified available outcomes; the transformations sum source entries with output indicators. In both predicates, normalization means finiteness on every nonsignaling correlation and zero on every local correlation, and monotonicity means nonincrease for every source and target scenario and every nonsignaling source correlation. Nonsignaling means nonnegative normalized entries and independence of each party’s marginal from the other party’s input.

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