Theorem 3 (18): non-contractivity of Sb under WPICC; original paper seed

Proved

QAlgorithms.Papers.Independent.Intakethird100.P29.wpicc_noncontractivity

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))$ . There exist scenarios, a WPICC wiring $W$ , and two behaviors $P,Q\in\mathrm{NS}$ on the initial scenario such that

S_b(W(P)\Vert W(Q))>S_b(P\Vert Q).

This separates operational box distinguishability from distinguishability obtained by fixing the two input settings before sampling outputs. The input boxes need not be nonlocal. 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.6, Theorem 3, (18); Appendix C, pp.12–13. No nonlocality premise.
The witness may use local boxes with one Bob input. -/
theorem wpicc_noncontractivity :
    ∃ (s t : BellScenario) (w : BellOperation s t) (p q : Behavior s),
      IsWPICC w ∧ IsNS p ∧ IsNS q ∧ sb p q < sb (w p) (w 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. 6, Theorem 3 (18)

Read-back

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

There exist scenarios $s,t$ , an operation $w$ from real behavior arrays on $s$ to those on $t$ , and nonsignaling correlations $p,q$ on $s$ , such that

S(p,q)<S(w(p),w(q)).

All scenario sizes are positive integers; a nonsignaling correlation is nonnegative, has total output mass one for each input pair, and has each party’s marginal independent of the other party’s input. Here

S(r,u)=\sup_{x,y}D(r_{xy}\Vert u_{xy}),\qquad D(P\Vert Q)= \begin{cases} \infty,&\exists i:\ P_i>0,\ Q_i=0,\\ \max\!\left\{0,\sum_iP_i\log(P_i/Q_i)\right\},&\text{otherwise}, \end{cases}

where $i$ ranges over output pairs, $\log$ is the natural logarithm, and the values lie in $[0,\infty]$ ; total real arithmetic uses $a/0=0$ and $\log 0=0$ . The operation $w$ agrees on every nonsignaling correlation with a probability mixture, over an arbitrary hidden-variable type, of deterministic transformations of these forms: independently choose the two source inputs from the respective target inputs and produce each final output from its own source outcome and target input; or fix Alice’s source 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 perform the symmetric Bob-first construction. All final outputs may depend on their own target inputs and the stated available outcomes; each deterministic transformation sums source entries with indicators enforcing its outputs. No restriction on $w$ outside nonsignaling correlations is asserted.

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