Prove2Me

Eq. (29): quantum non-signalling for the GHZ state

Proved
DrezetGHZ.ghz_nonsignaling

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

ghzquantum-foundations

For the GHZ state ∣ψ⟩|\psi\rangle and settings in {x^,y^}\{\hat x,\hat y\}:

  1. Non-signalling (Eq. (29)). Alice's marginal does not depend on Bob's and Charlie's settings: for all n^1,n^2,n^3,n^2′,n^3′\hat n_1,\hat n_2,\hat n_3,\hat n_2',\hat n_3' and α∈{±1}\alpha\in\{\pm1\},
∑β,γP(α,β,γ∣n^1,n^2,n^3,ψ)=∑β,γP(α,β,γ∣n^1,n^2′,n^3′,ψ).\sum_{\beta,\gamma}P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3,\psi)=\sum_{\beta,\gamma}P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2',\hat n_3',\psi).
  1. Alice's x^\hat x-marginal is uniform: for all n^2,n^3\hat n_2,\hat n_3 and α\alpha,
P1(α∣x^,ψ)=∑β,γP(α,β,γ∣x^,n^2,n^3,ψ)=12.P_1(\alpha\mid\hat x,\psi)=\sum_{\beta,\gamma}P(\alpha,\beta,\gamma\mid\hat x,\hat n_2,\hat n_3,\psi)=\tfrac12.

The paper cites this as the non-signalling property that advocates of Everettian locality appeal to, and which it distinguishes from Bell's local causality.

Preamble
import Mathlib
import Definitions.Def_DrezetGHZ_Quantum
Formal statement
namespace DrezetGHZ
theorem ghz_nonsignaling :
    (∀ (n₁ n₂ n₃ n₂' n₃' : Setting) (α : ℤˣ),
      ∑ β, ∑ γ, bornProb n₁ n₂ n₃ α β γ = ∑ β, ∑ γ, bornProb n₁ n₂' n₃' α β γ) ∧
    (∀ (n₂ n₃ : Setting) (α : ℤˣ), ∑ β, ∑ γ, bornProb .x n₂ n₃ α β γ = 1 / 2) := 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, Eq. (29); p. 11: "there are only two worlds ∣A+1x⟩|A_{+1_x}\rangle, ∣A−1x⟩|A_{-1_x}\rangle with the same probability P1(±1∣x^,ψ)=1/2P_1(\pm1\mid\hat x,\psi)=1/2 … This probability is independent of the measurement choices made by Bob and Charlie".
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. Both of the following hold:

  1. 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\},
∑β∑γbornProb(n1,n2,n3;α,β,γ)=∑β∑γbornProb(n1,n2′,n3′;α,β,γ);\sum_{\beta}\sum_{\gamma}\mathrm{bornProb}(n_1,n_2,n_3;\alpha,\beta,\gamma)=\sum_{\beta}\sum_{\gamma}\mathrm{bornProb}(n_1,n_2',n_3';\alpha,\beta,\gamma);
  1. for all settings n2,n3n_2,n_3 and every α\alpha, ∑β∑γbornProb(x,n2,n3;α,β,γ)=1/2\sum_\beta\sum_\gamma\mathrm{bornProb}(x,n_2,n_3;\alpha,\beta,\gamma)=1/2.

The sums run over β,γ∈{±1}\beta,\gamma\in\{\pm1\}. bornProb\mathrm{bornProb} is the Born probability for the state ψ=(∣000⟩−∣111⟩)/2\psi=(|000\rangle-|111\rangle)/\sqrt2 with the eigenvectors ex,a=(1,a)/2e_{x,a}=(1,a)/\sqrt2 and ey,a=(1,ia)/2e_{y,a}=(1,ia)/\sqrt2. Part 2 is stated only for Alice's setting xx. There are no hypotheses.

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