Prove2Me

GHZ Born probabilities for the four GHZ settings

Proved
DrezetGHZ.ghz_born_probabilities

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

ghzquantum-foundations

For every triple of outcomes α,β,γ∈{±1}\alpha,\beta,\gamma\in\{\pm1\}, the Born probabilities of the GHZ state are

P(α,β,γ∣x^,x^,x^,ψ)={14αβγ=−10otherwise,P(\alpha,\beta,\gamma\mid\hat x,\hat x,\hat x,\psi)=\begin{cases}\tfrac14&\alpha\beta\gamma=-1\\0&\text{otherwise,}\end{cases}

and, for each of the settings (x^,y^,y^)(\hat x,\hat y,\hat y), (y^,x^,y^)(\hat y,\hat x,\hat y) and (y^,y^,x^)(\hat y,\hat y,\hat x),

P(α,β,γ∣n^1,n^2,n^3,ψ)={14αβγ=+10otherwise.P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3,\psi)=\begin{cases}\tfrac14&\alpha\beta\gamma=+1\\0&\text{otherwise.}\end{cases}

So in each GHZ experiment exactly four of the 232^3 outcome triples occur, each with probability 1/41/4.

Preamble
import Mathlib
import Definitions.Def_DrezetGHZ_Quantum
Formal statement
namespace DrezetGHZ
theorem ghz_born_probabilities (α β γ : ℤˣ) :
    bornProb .x .x .x α β γ = (if α * β * γ = -1 then 1 / 4 else 0) ∧
    bornProb .x .y .y α β γ = (if α * β * γ = 1 then 1 / 4 else 0) ∧
    bornProb .y .x .y α β γ = (if α * β * γ = 1 then 1 / 4 else 0) ∧
    bornProb .y .y .x α β γ = (if α * β * γ = 1 then 1 / 4 else 0) := 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 (after Eq. (29): ∣Aα,β,γ∣2=1/4|A_{\alpha,\beta,\gamma}|^2=1/4 iff αβγ=−1\alpha\beta\gamma=-1), p. 11 (after Eq. (32): ∣Bα,β,γ∣2=1/4|B_{\alpha,\beta,\gamma}|^2=1/4 iff αβγ=+1\alpha\beta\gamma=+1), and p. 13 (four possible triplets per GHZ game).
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. For all α,β,γ∈Z×={±1}\alpha,\beta,\gamma\in\mathbb Z^\times=\{\pm1\}, all four of the following equalities of real numbers hold:

  1. bornProb(x,x,x;α,β,γ)=1/4\mathrm{bornProb}(x,x,x;\alpha,\beta,\gamma)=1/4 if αβγ=−1\alpha\beta\gamma=-1, and 00 otherwise;
  2. bornProb(x,y,y;α,β,γ)=1/4\mathrm{bornProb}(x,y,y;\alpha,\beta,\gamma)=1/4 if αβγ=1\alpha\beta\gamma=1, and 00 otherwise;
  3. bornProb(y,x,y;α,β,γ)=1/4\mathrm{bornProb}(y,x,y;\alpha,\beta,\gamma)=1/4 if αβγ=1\alpha\beta\gamma=1, and 00 otherwise;
  4. bornProb(y,y,x;α,β,γ)=1/4\mathrm{bornProb}(y,y,x;\alpha,\beta,\gamma)=1/4 if αβγ=1\alpha\beta\gamma=1, and 00 otherwise.

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