Unnumbered main result: LOSR inclusion and strict separation, (9),(11)

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.wiring_inclusions_and_separation

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. For every pair of scenarios, every LOSR wiring is both a WPICC wiring and a global wiring. Moreover, there are scenarios and a WPICC wiring for which no LOSR wiring agrees on all no-signaling inputs:

\mathrm{LOSR}\subseteq\mathrm{WPICC},\qquad \mathrm{LOSR}\subseteq\mathrm{GW},\qquad\exists W\in\mathrm{WPICC}:W\notin\mathrm{LOSR}.

Strictness is existential over scenarios; no strict separation is asserted for degenerate fixed scenarios. 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.4, (9),(11), and p.6 strict separation: both inclusions hold in every
scenario pair, while strict LOSR/WPICC separation is existential over scenarios.
The witness is separated extensionally on the common NS domain. -/
theorem wiring_inclusions_and_separation :
    (∀ (s t : BellScenario) (w : BellOperation s t),
      IsLOSR w → IsWPICC w ∧ IsGW w) ∧
    (∃ (s t : BellScenario) (w : BellOperation s t),
      IsWPICC w ∧ ¬ HasLOSRRestriction w) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 4, Equations (9),(11); strictness p.6

Read-back

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

A Bell scenario here has finite nonempty question and answer sets. For source sets $X,Y,A,B$ and target sets $X',Y',A',B'$ , call an operation LOSR when, on every real source array, it has the form

(wr)(\chi,\psi,\alpha,\beta)= \sum_{a,b,x,y} \mathbb E_j[O^j_A(\alpha\mid a,x,\chi)O^j_B(\beta\mid b,y,\psi)]\, r(x,y,a,b)\, \mathbb E_h[I^h_A(x\mid\chi)I^h_B(y\mid\psi)],

where the two expectations use discrete probability mass functions on arbitrary hidden-variable sets and every input and output kernel is nonnegative and normalized. Call an operation WPICC when, on every nonnegative normalized nonsignaling array—meaning each answer marginal is independent of the other party’s question—it agrees with a discrete probability mixture of deterministic preparations of three kinds: both source questions are local functions of the target questions and both target answers are local functions of the target question and source answer; Alice first uses a fixed source question and her answer selects either a continuation where Bob’s source question depends on his target question, Alice outputs from her target question, and Bob outputs from his target question and source answer, or a continuation where Bob uses a fixed source question and both outputs depend on Bob’s source answer and the respective target question; or the corresponding Bob-first preparation. All continuation data may depend on the first answer, and probabilities are the sums of source probabilities selected by these rules. Call an operation a global wiring when, on every real array, it has the form

(wr)(\chi,\psi,\alpha,\beta)= \sum_{a,b,x,y}O(\alpha,\beta\mid a,b,x,y,\chi,\psi)\, r(x,y,a,b)I(x,y\mid\chi,\psi),

with arbitrary normalized nonnegative joint kernels $I,O$ . The declaration asserts that, for every pair of Bell scenarios and every operation between them, being LOSR implies both being WPICC and being a global wiring. It also asserts the existence of two Bell scenarios and a WPICC operation $w$ between them for which there is no LOSR operation $v$ satisfying $wp=vp$ for every nonsignaling source array $p$ .

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