Prove2Me

GHZ theorem: no locally causal model reproduces the GHZ predictions

Proved
DrezetGHZ.ghz_not_bell_local

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

bell-nonlocalityghzquantum-foundations

GHZ nonlocality theorem (Bell-locality form). Let Λ\Lambda be any measurable space of beables, and consider any locally causal model on it: a setting-independent probability measure ρ\rho on Λ\Lambda (Eq. (18)), together with measurable local response probabilities Pj(α∣λ,n^j)P_j(\alpha\mid\lambda,\hat n_j) (Eq. (17)). Then it is not the case that, for all four GHZ settings (x^,x^,x^)(\hat x,\hat x,\hat x), (x^,y^,y^)(\hat x,\hat y,\hat y), (y^,x^,y^)(\hat y,\hat x,\hat y), (y^,y^,x^)(\hat y,\hat y,\hat x) and all outcomes α,β,γ∈{±1}\alpha,\beta,\gamma\in\{\pm1\},

∫ΛP1(α∣λ,n^1)P2(β∣λ,n^2)P3(γ∣λ,n^3) dρ(λ)=∣⟨αn^1βn^2γn^3∣ψ⟩∣2,\int_\Lambda P_1(\alpha\mid\lambda,\hat n_1)P_2(\beta\mid\lambda,\hat n_2)P_3(\gamma\mid\lambda,\hat n_3)\,d\rho(\lambda)=\big|\langle\alpha_{\hat n_1}\beta_{\hat n_2}\gamma_{\hat n_3}\mid\psi\rangle\big|^2,

where ∣ψ⟩|\psi\rangle is the GHZ state of Eq. (1).

This is the result from which the paper concludes that quantum mechanics, and hence Everett's theory, is not locally causal in Bell's sense, whether or not the beables are hidden variables.

Formalization Note The beables are fully general, since Λ\Lambda is any measurable space. Only the four GHZ setting triples are constrained.

Preamble
import Mathlib
import Definitions.Def_DrezetGHZ_Models
Formal statement
namespace DrezetGHZ
theorem ghz_not_bell_local {Λ : Type*} [MeasurableSpace Λ] (M : LocalCausalModel Λ) :
    ¬ ((∀ α β γ : ℤˣ, M.predict .x .x .x α β γ = bornProb .x .x .x α β γ) ∧
       (∀ α β γ : ℤˣ, M.predict .x .y .y α β γ = bornProb .x .y .y α β γ) ∧
       (∀ α β γ : ℤˣ, M.predict .y .x .y α β γ = bornProb .y .x .y α β γ) ∧
       (∀ α β γ : ℤˣ, M.predict .y .y .x α β γ = bornProb .y .y .x α β γ)) := 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, Section II, pp. 2–7: Eqs. (1)–(5), (10)–(13), (14), (17)–(18), (19)–(27) and summary (i)–(iii) on p. 7.
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 any type with a σ-algebra, and let MM be any locally causal model on Λ\Lambda. Such a model has a probability measure ρ\rho that does not depend on settings, and measurable response functions Pj(λ,n,α)∈[0,1]P_j(\lambda,n,\alpha)\in[0,1] for j∈{0,1,2}j\in\{0,1,2\}, n∈{x,y}n\in\{x,y\}, α∈{±1}\alpha\in\{\pm1\}, with ∑αPj=1\sum_\alpha P_j=1. Write 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.

The theorem asserts that the conjunction of the following four statements is false:

  1. for all α,β,γ∈{±1}\alpha,\beta,\gamma\in\{\pm1\}, predM(x,x,x;α,β,γ)=bornProb(x,x,x;α,β,γ)\mathrm{pred}_M(x,x,x;\alpha,\beta,\gamma)=\mathrm{bornProb}(x,x,x;\alpha,\beta,\gamma);
  2. the same equality for all outcomes with settings (x,y,y)(x,y,y);
  3. the same equality for all outcomes with settings (y,x,y)(y,x,y);
  4. the same equality for all outcomes with settings (y,y,x)(y,y,x).

Here bornProb(n1,n2,n3;α,β,γ)=∣⟨en1,α⊗en2,β⊗en3,γ,ψ⟩∣2\mathrm{bornProb}(n_1,n_2,n_3;\alpha,\beta,\gamma)=|\langle e_{n_1,\alpha}\otimes e_{n_2,\beta}\otimes e_{n_3,\gamma},\psi\rangle|^2, with ψ=(∣000⟩−∣111⟩)/2\psi=(|000\rangle-|111\rangle)/\sqrt2, ex,a=(1,a)/2e_{x,a}=(1,a)/\sqrt2 and ey,a=(1,ia)/2e_{y,a}=(1,ia)/\sqrt2.

Edge cases. Λ\Lambda is arbitrary; it is nonempty because it carries a probability measure. The other four setting triples are not constrained. Nothing is assumed beyond the model's own axioms.

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