Prove2Me

Local causality implies non-signalling

Proved
DrezetGHZ.local_causality_implies_nonsignaling

by Lucas · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

bell-nonlocalityquantum-foundations

Let MM be a locally causal model (Eqs. (14), (17), (18)). For every setting n^1\hat n_1 of Alice, every outcome α\alpha, and any two choices (n^2,n^3)(\hat n_2,\hat n_3) and (n^2′,n^3′)(\hat n_2',\hat n_3') of Bob's and Charlie's settings,

∑β,γ=±1P(α,β,γ∣n^1,n^2,n^3)=∑β,γ=±1P(α,β,γ∣n^1,n^2′,n^3′).\sum_{\beta,\gamma=\pm1}P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3)=\sum_{\beta,\gamma=\pm1}P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2',\hat n_3').

Alice's marginal statistics therefore do not depend on the distant settings. The paper uses this to argue that non-signalling cannot distinguish local causality from quantum mechanics.

Preamble
import Mathlib
import Definitions.Def_DrezetGHZ_Models
Formal statement
namespace DrezetGHZ
theorem local_causality_implies_nonsignaling {Λ : Type*} [MeasurableSpace Λ]
    (M : LocalCausalModel Λ) (n₁ n₂ n₃ n₂' n₃' : Setting) (α : ℤˣ) :
    ∑ β, ∑ γ, M.predict n₁ n₂ n₃ α β γ = ∑ β, ∑ γ, M.predict n₁ n₂' n₃' α β γ := by sorry
end DrezetGHZ
Source
A. Drezet, "An Elementary Proof That Everett's Quantum Multiverse Is Nonlocal: Bell-Locality and Branch-Symmetry in the Many-Worlds Interpretation", arXiv:2306.07794v1 [quant-ph] (2023), https://arxiv.org/abs/2306.07794, p. 10: "Clearly, local-causality implies nonsignaling, but the opposite is not always true" (following Eq. (29)).
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements of this proposal, with full knowledge of the source paper and of the intended meaning. It is not a blind, independent audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves.

Statement. Let Λ\Lambda be a type with a σ-algebra and MM a locally causal model on it (a probability measure ρ\rho and measurable responses Pj(λ,n,α)∈[0,1]P_j(\lambda,n,\alpha)\in[0,1] summing to 11 over α\alpha). For all settings n1,n2,n3,n2′,n3′∈{x,y}n_1,n_2,n_3,n_2',n_3'\in\{x,y\} and every α∈{±1}\alpha\in\{\pm1\},

∑β∈{±1}∑γ∈{±1}predM(n1,n2,n3;α,β,γ)=∑β∑γpredM(n1,n2′,n3′;α,β,γ),\sum_{\beta\in\{\pm1\}}\sum_{\gamma\in\{\pm1\}}\mathrm{pred}_M(n_1,n_2,n_3;\alpha,\beta,\gamma)=\sum_{\beta}\sum_{\gamma}\mathrm{pred}_M(n_1,n_2',n_3';\alpha,\beta,\gamma),

where predM(n1,n2,n3;α,β,γ)=∫P0(λ,n1,α)P1(λ,n2,β)P2(λ,n3,γ) dρ\mathrm{pred}_M(n_1,n_2,n_3;\alpha,\beta,\gamma)=\int P_0(\lambda,n_1,\alpha)P_1(\lambda,n_2,\beta)P_2(\lambda,n_3,\gamma)\,d\rho.

Only Alice's (party 00) marginal is covered. The statement says nothing about the marginals of Bob and Charlie.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph