Lemma 13 (G3): decomposition of LOSR into UCLOSR mixtures

Open

QAlgorithms.Papers.Independent.Intakethird100.P29.losr_finite_uncorrelated_decomposition

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 LOSR operation $W$ , there are a positive integer $n$ , nonnegative weights $w_1,\ldots,w_n$ summing to one, and UCLOSR operations $U_1,\ldots,U_n$ such that, simultaneously for every input behavior,

W(P)=\sum_{k=1}^n w_k U_k(P).

The weights and operations are independent of $P$ . This is a decomposition of an operation, and includes the finite reduction of the accepted arbitrary-discrete shared-randomness interface.

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.15, Lemma 13, (G3). This also asserts the finite reduction of the
accepted arbitrary-discrete two-local-box interface: finite seed size, weights,
and components are chosen before *all* raw behaviors simultaneously.
No finite-support assumption is made on the original shared-variable laws. -/
theorem losr_finite_uncorrelated_decomposition {s t : BellScenario}
    (w : BellOperation s t) (hw : IsLOSR w) :
    ∃ (n : ℕ) (_hn : 0 < n) (weights : Fin n → ℝ)
      (u : Fin n → UncorrelatedWiring s t),
      IsLaw weights ∧ ∀ p chi psi alpha beta,
        w p chi psi alpha beta =
          ∑ k, weights k * (u k).apply p chi psi alpha beta := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P29

end

Source

Nonlocality free wirings and the distinguishability between Bell boxes, arXiv:1611.06932v2, PDF p. 15, Lemma 13 (G3)

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 $X,Y,A,B$ and $X',Y',A',B'$ . Let $w$ be a function from all real source arrays $r(x,y,a,b)$ to real target arrays. Assume $w$ admits the following representation on every real array: there are arbitrary hidden-variable sets with discrete probability mass functions $\pi_{\mathrm{in}},\pi_{\mathrm{out}}$ , normalized nonnegative input kernels $I^h_A(x\mid\chi),I^h_B(y\mid\psi)$ , and normalized nonnegative output kernels $O^j_A(\alpha\mid a,x,\chi),O^j_B(\beta\mid b,y,\psi)$ , such that

(wr)(\chi,\psi,\alpha,\beta)= \sum_{a,b,x,y} \left(\sum_j\pi_{\mathrm{out}}(j)O^j_A(\alpha\mid a,x,\chi)O^j_B(\beta\mid b,y,\psi)\right) r(x,y,a,b) \left(\sum_h\pi_{\mathrm{in}}(h)I^h_A(x\mid\chi)I^h_B(y\mid\psi)\right).

Then there exist a positive integer $n$ , real weights $\lambda_0,\ldots,\lambda_{n-1}$ with $\lambda_k\ge0$ and $\sum_k\lambda_k=1$ , and $n$ transformations $u_k$ , each having the form

(u_kr)(\chi,\psi,\alpha,\beta)= \sum_{a,b,x,y} O_{A,k}(\alpha\mid a,x,\chi)O_{B,k}(\beta\mid b,y,\psi)\, r(x,y,a,b)I_{A,k}(x\mid\chi)I_{B,k}(y\mid\psi)

for normalized nonnegative kernels, such that $(wr)(\chi,\psi,\alpha,\beta)=\sum_{k=0}^{n-1}\lambda_k(u_kr)(\chi,\psi,\alpha,\beta)$ for every real source array and every target question and answer tuple. Zero weights are allowed, but $n=0$ is excluded.

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