Prove2Me

Eqs. (2)–(5): the GHZ state is an eigenvector of σxσxσx\sigma_x\sigma_x\sigma_x and of the σxσyσy\sigma_x\sigma_y\sigma_y-type operators

Proved
DrezetGHZ.ghz_eigen_relations

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

ghzquantum-foundations

Let ∣ψ⟩=12(∣+z+z+z⟩−∣−z−z−z⟩)|\psi\rangle=\frac1{\sqrt2}(|{+z}{+z}{+z}\rangle-|{-z}{-z}{-z}\rangle) be the GHZ state. Then

σx(1)σx(2)σx(3)∣ψ⟩=−∣ψ⟩,σx(1)σy(2)σy(3)∣ψ⟩=∣ψ⟩,\sigma_x^{(1)}\sigma_x^{(2)}\sigma_x^{(3)}|\psi\rangle=-|\psi\rangle,\qquad \sigma_x^{(1)}\sigma_y^{(2)}\sigma_y^{(3)}|\psi\rangle=|\psi\rangle, σy(1)σx(2)σy(3)∣ψ⟩=∣ψ⟩,σy(1)σy(2)σx(3)∣ψ⟩=∣ψ⟩.\sigma_y^{(1)}\sigma_x^{(2)}\sigma_y^{(3)}|\psi\rangle=|\psi\rangle,\qquad \sigma_y^{(1)}\sigma_y^{(2)}\sigma_x^{(3)}|\psi\rangle=|\psi\rangle.

These four eigenvalue relations are the perfect correlations on which the GHZ argument rests.

Preamble
import Mathlib
import Definitions.Def_DrezetGHZ_Quantum
open Matrix
Formal statement
namespace DrezetGHZ
theorem ghz_eigen_relations :
    tensor3 pauliX pauliX pauliX *ᵥ ghzState = -ghzState ∧
    tensor3 pauliX pauliY pauliY *ᵥ ghzState = ghzState ∧
    tensor3 pauliY pauliX pauliY *ᵥ ghzState = ghzState ∧
    tensor3 pauliY pauliY pauliX *ᵥ ghzState = ghzState := 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. (2)–(5).
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. With σx=(0110)\sigma_x=\begin{pmatrix}0&1\\1&0\end{pmatrix}, σy=(0−ii0)\sigma_y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix}, ψ:{0,1}3→C\psi:\{0,1\}^3\to\mathbb C given by ψ(000)=1/2\psi(000)=1/\sqrt2, ψ(111)=−1/2\psi(111)=-1/\sqrt2 and ψ=0\psi=0 elsewhere, and A⊗B⊗CA\otimes B\otimes C the Kronecker product A⊗(B⊗C)A\otimes(B\otimes C) acting on vectors by matrix–vector multiplication, all four of the following equalities of vectors in C{0,1}3\mathbb C^{\{0,1\}^3} hold:

(σx⊗σx⊗σx)ψ=−ψ,(σx⊗σy⊗σy)ψ=ψ,(σy⊗σx⊗σy)ψ=ψ,(σy⊗σy⊗σx)ψ=ψ.(\sigma_x\otimes\sigma_x\otimes\sigma_x)\psi=-\psi,\quad(\sigma_x\otimes\sigma_y\otimes\sigma_y)\psi=\psi,\quad(\sigma_y\otimes\sigma_x\otimes\sigma_y)\psi=\psi,\quad(\sigma_y\otimes\sigma_y\otimes\sigma_x)\psi=\psi.

There are no hypotheses and no free variables.

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