Prove2Me

Eqs. (10)–(13): the GHZ constraints admit no ±1 assignment

Proved
DrezetGHZ.ghz_no_deterministic_assignment

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

ghzquantum-foundations

There are no values A1,A2,A3,B1,B2,B3∈{+1,−1}A_1,A_2,A_3,B_1,B_2,B_3\in\{+1,-1\} such that

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

This is the GHZ contradiction: the product of the last three constraints is A1A2A3=+1A_1A_2A_3=+1, which conflicts with the first.

Formalization Note Values in {±1}\{\pm1\} are elements of ℤˣ. Parties 1,2,31,2,3 are indices 0,1,20,1,2.

Preamble
import Mathlib
Formal statement
namespace DrezetGHZ
theorem ghz_no_deterministic_assignment :
    ¬ ∃ A B : Fin 3 → ℤˣ,
      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. 3 Eqs. (6)–(9) and p. 4 Eqs. (10)–(13).
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. There do not exist functions A,B:{0,1,2}→Z×A,B:\{0,1,2\}\to\mathbb Z^\times (so every value is +1+1 or −1-1) satisfying all four of

A0A1A2=−1,A0B1B2=1,B0A1B2=1,B0B1A2=1.A_0A_1A_2=-1,\qquad A_0B_1B_2=1,\qquad B_0A_1B_2=1,\qquad B_0B_1A_2=1.

There are no hypotheses.

View graph