Eqs. (19)–(27): perfect GHZ correlations force local determinism

Proved

DrezetGHZ.product_supported_implies_deterministic

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

ghzquantum-foundations

Let $p_1,p_2,p_3$ be probability distributions on $\{+1,-1\}$ (nonnegative, summing to $1$ ), and let $s\in\{\pm1\}$ . Suppose that

p_1(\alpha)\,p_2(\beta)\,p_3(\gamma)=0\quad\text{whenever }\alpha\beta\gamma\neq s.

Then there are $a_1,a_2,a_3\in\{\pm1\}$ with $a_1a_2a_3=s$ such that each $p_j$ is the point mass at $a_j$ : $p_j(\alpha)=1$ if $\alpha=a_j$ , and $p_j(\alpha)=0$ otherwise.

This is the step in which locality combined with the perfect GHZ correlations yields determinism, $P_j(\alpha\mid\lambda,\hat n)=\delta_{\alpha,A_j(\lambda)}$ (Eq. (27)), applied at a fixed beable $\lambda$ .

Preamble

import Mathlib

Formal statement

namespace DrezetGHZ
theorem product_supported_implies_deterministic (p₁ p₂ p₃ : ℤˣ → ℝ) (s : ℤˣ)
    (h₁ : ∀ α, 0 ≤ p₁ α) (h₂ : ∀ α, 0 ≤ p₂ α) (h₃ : ∀ α, 0 ≤ p₃ α)
    (hs₁ : ∑ α, p₁ α = 1) (hs₂ : ∑ α, p₂ α = 1) (hs₃ : ∑ α, p₃ α = 1)
    (hzero : ∀ α β γ : ℤˣ, α * β * γ ≠ s → p₁ α * p₂ β * p₃ γ = 0) :
    ∃ a₁ a₂ a₃ : ℤˣ, a₁ * a₂ * a₃ = s ∧
      (∀ α, p₁ α = if α = a₁ then 1 else 0) ∧
      (∀ α, p₂ α = if α = a₂ then 1 else 0) ∧
      (∀ α, p₃ α = if α = a₃ then 1 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, pp. 6–7, Eqs. (19)–(27).

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 $p_1,p_2,p_3:\{\pm1\}\to\mathbb R$ and $s\in\{\pm1\}$ . Assume:

$p_1(\alpha)\ge0$ , $p_2(\alpha)\ge0$ and $p_3(\alpha)\ge0$ for all $\alpha$ ;
$p_1(1)+p_1(-1)=1$ , and the same for $p_2$ and $p_3$ ;
for all $\alpha,\beta,\gamma\in\{\pm1\}$ with $\alpha\beta\gamma\neq s$ , $p_1(\alpha)p_2(\beta)p_3(\gamma)=0$ .

Then there exist $a_1,a_2,a_3\in\{\pm1\}$ with $a_1a_2a_3=s$ such that, for every $\alpha$ , $p_1(\alpha)$ is $1$ if $\alpha=a_1$ and $0$ otherwise, and likewise $p_2$ with $a_2$ and $p_3$ with $a_3$ .

Edge cases. $s$ ranges over both signs. The hypotheses are satisfiable, for example by point masses whose product is $s$ .

View graph