Unnumbered result in Lemma 6 proof: pointwise LOSR simulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.pointwise_losr_simulation

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 WPICC wiring $W$ and every fixed no-signaling behavior $P$ , there is an LOSR wiring $V$ such that

W(P)=V(P).

The quantifier order is $\forall W\,\forall P\,\exists V$ : the simulator may depend on the fixed input box. This pointwise assertion does not identify the classes of operations. 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, proof of Lemma 6: the simulating LOSR map may depend on this
specific input behavior, unlike an equality between classes of operations. -/
theorem pointwise_losr_simulation {s t : BellScenario} (w : BellOperation s t)
    (hw : IsWPICC w) (p : Behavior s) (hp : IsNS p) :
    ∃ v : BellOperation s t, IsLOSR v ∧ w p = v 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. 6, Proof of Lemma 6

Read-back

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

Let $s,t$ be any Bell scenarios with finite nonempty question and answer sets, and let $w$ be an operation on real arrays. Assume that, on nonnegative normalized nonsignaling arrays, $w$ is a discrete probability mixture over an arbitrary hidden-variable set of deterministic preparations of the following forms: both source questions depend only on the respective target question and both target answers depend only on the respective target question and source answer; Alice first uses a fixed source question and her answer selects either a continuation where Bob waits to choose his source question from 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 his source answer and the respective target question; or the corresponding Bob-first preparation. Continuation choices and functions may depend on the first answer, and output probabilities are obtained by summing source probabilities consistent with the deterministic outputs. Fix any source array $p$ that is nonnegative, normalized over answers for every question pair, and has each answer marginal independent of the other party’s question. Then there exists an operation $v$ such that $wp=vp$ , and such that, for every real source array $r$ ,

(vr)(\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 sets and all input and output kernels are nonnegative and normalized. The operation $v$ may depend on the chosen $p$ ; the asserted equality is at that $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