Unnumbered result: a GW can convert any behavior into any other

Proved

QAlgorithms.Papers.Independent.Intakethird100.P29.global_replacement

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 any normalized initial behavior $P$ and any normalized target behavior $Q$ , on possibly different scenarios, there exists a global wiring $G$ such that

G(P)=Q.

Both behaviors may be signaling. The operation may depend on the chosen target, as in the source’s constant-output-kernel construction.

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, after (11): arbitrary normalized behaviors, including signaling
ones, can be replaced by a target-dependent GW. -/
theorem global_replacement {s t : BellScenario} (p : Behavior s) (q : Behavior t)
    (hp : IsCorrelation p) (hq : IsCorrelation q) :
    ∃ g : GlobalWiring s t, g.apply p = 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. 4, Unnumbered result after (11)

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 $p(x,y,a,b)$ and $q(\chi,\psi,\alpha,\beta)$ be real arrays satisfying nonnegativity and answer normalization at every question pair: $\sum_{a,b}p(x,y,a,b)=1$ and $\sum_{\alpha,\beta}q(\chi,\psi,\alpha,\beta)=1$ . Then there exist nonnegative joint kernels $I(x,y\mid\chi,\psi)$ and $O(\alpha,\beta\mid a,b,x,y,\chi,\psi)$ , each summing to one over its output variables for every choice of conditioning variables, such that

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

for every target question and answer tuple. Neither $p$ nor $q$ is assumed to have question-independent opposite-party marginals.

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