Prove2Me

Section II (ii): a locally causal model reproducing GHZ is almost surely deterministic

Proved
DrezetGHZ.local_model_reproducing_ghz_is_deterministic

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

bell-nonlocalityghzquantum-foundations

Let MM be a locally causal model on a measurable space Λ\Lambda, with setting-independent probability measure ρ\rho and local responses Pj(α∣λ,n^)P_j(\alpha\mid\lambda,\hat n). Suppose MM reproduces the GHZ Born probabilities for all outcomes in each of the four 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).

Then for ρ\rho-almost every λ\lambda there are values A1,A2,A3,B1,B2,B3∈{±1}A_1,A_2,A_3,B_1,B_2,B_3\in\{\pm1\} such that

Pj(α∣λ,x^)=δα,Aj,Pj(α∣λ,y^)=δα,Bj(j=1,2,3),P_j(\alpha\mid\lambda,\hat x)=\delta_{\alpha,A_j},\qquad P_j(\alpha\mid\lambda,\hat y)=\delta_{\alpha,B_j}\qquad(j=1,2,3),

and

A1A2A3=−1,A1B2B3=+1,B1A2B3=+1,B1B2A3=+1.A_1A_2A_3=-1,\quad A_1B_2B_3=+1,\quad B_1A_2B_3=+1,\quad B_1B_2A_3=+1.

This is Eq. (27) together with the GHZ constraints (10)–(13), established for almost every beable.

Preamble
import Mathlib
import Definitions.Def_DrezetGHZ_Models
open MeasureTheory
Formal statement
namespace DrezetGHZ
theorem local_model_reproducing_ghz_is_deterministic {Λ : Type*} [MeasurableSpace Λ]
    (M : LocalCausalModel Λ)
    (hxxx : ∀ α β γ : ℤˣ, M.predict .x .x .x α β γ = bornProb .x .x .x α β γ)
    (hxyy : ∀ α β γ : ℤˣ, M.predict .x .y .y α β γ = bornProb .x .y .y α β γ)
    (hyxy : ∀ α β γ : ℤˣ, M.predict .y .x .y α β γ = bornProb .y .x .y α β γ)
    (hyyx : ∀ α β γ : ℤˣ, M.predict .y .y .x α β γ = bornProb .y .y .x α β γ) :
    ∀ᵐ lam ∂M.ρ, ∃ A B : Fin 3 → ℤˣ,
      (∀ j α, M.P j lam .x α = if α = A j then 1 else 0) ∧
      (∀ j α, M.P j lam .y α = if α = B j then 1 else 0) ∧
      A 0 * A 1 * A 2 = -1 ∧
      A 0 * B 1 * B 2 = 1 ∧
      B 0 * A 1 * B 2 = 1 ∧
      B 0 * B 1 * A 2 = 1 := 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. 7, Eq. (27) and summary point (ii): "for the GHZ state, locality added to quantum mechanics implies determinism"; together with Eqs. (10)–(13) on p. 4.
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, with probability measure ρ\rho and measurable responses Pj(λ,n,α)∈[0,1]P_j(\lambda,n,\alpha)\in[0,1], ∑αPj=1\sum_\alpha P_j=1. Assume four hypotheses: 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),
  • and the same equality for the settings (x,y,y)(x,y,y), (y,x,y)(y,x,y) and (y,y,x)(y,y,x).

Here 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.

Conclusion. For ρ\rho-almost every λ\lambda (all λ\lambda outside a ρ\rho-null set), there exist A,B:{0,1,2}→{±1}A,B:\{0,1,2\}\to\{\pm1\} such that:

  • for every j∈{0,1,2}j\in\{0,1,2\} and α\alpha: Pj(λ,x,α)=1P_j(\lambda,x,\alpha)=1 if α=Aj\alpha=A_j and 00 otherwise;
  • for every jj and α\alpha: Pj(λ,y,α)=1P_j(\lambda,y,\alpha)=1 if α=Bj\alpha=B_j and 00 otherwise;
  • A0A1A2=−1A_0A_1A_2=-1, A0B1B2=1A_0B_1B_2=1, B0A1B2=1B_0A_1B_2=1 and B0B1A2=1B_0B_1A_2=1.

Edge cases. The conclusion is an almost-everywhere statement, so if the hypotheses cannot be satisfied (as the goal theorem asserts) the statement holds vacuously. As a milestone it is the intermediate step and is stated in exactly this conditional form.

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