Appendix 3, Eqs. (39)–(45): a setting-dependent beable model reproduces the GHZ predictions

Proved

DrezetGHZ.appendix_superdeterministic_model_reproduces_ghz

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

ghzquantum-foundationssuperdeterminism

Consider the model of Appendix 3. The beables are angle triples $(\theta_1,\theta_2,\theta_3)$ . The local responses are

P_j(\alpha\mid\theta_j,\hat x)=\tfrac{1+\alpha\cos\theta_j}{2},\qquad P_j(\alpha\mid\theta_j,\hat y)=\tfrac{1+\alpha\sin\theta_j}{2}\qquad\text{(Eq. (43)),}

and the setting-dependent density is

\rho(\cdot\mid\hat n_1,\hat n_2,\hat n_3)=\tfrac14\sum_{v_1v_2v_3=s}\delta_{(\vartheta(\hat n_1,v_1),\vartheta(\hat n_2,v_2),\vartheta(\hat n_3,v_3))}\qquad\text{(Eqs. (44)–(45)),}

where $s=-1$ for $(\hat x,\hat x,\hat x)$ , $s=+1$ for the other three GHZ settings, and $\vartheta(\pm\hat x)\in\{0,\pi\}$ , $\vartheta(\pm\hat y)=\pm\pi/2$ are polar angles.

Then for each of the four GHZ settings $(\hat n_1,\hat n_2,\hat n_3)$ and all $\alpha,\beta,\gamma\in\{\pm1\}$ ,

\int P_1(\alpha\mid\theta_1,\hat n_1)P_2(\beta\mid\theta_2,\hat n_2)P_3(\gamma\mid\theta_3,\hat n_3)\,d\rho(\theta\mid\hat n_1,\hat n_2,\hat n_3)=P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3,\psi)

(Eqs. (39)–(42)).

The model keeps the local factorization of Eq. (17) and gives up statistical independence (Eq. (18)). This is the paper's example that the GHZ correlations can be reproduced once superdeterminism is allowed.

Preamble

import Mathlib
import Definitions.Def_DrezetGHZ_Models
open MeasureTheory

Formal statement

namespace DrezetGHZ
theorem appendix_superdeterministic_model_reproduces_ghz (n₁ n₂ n₃ : Setting)
    (hn : (n₁, n₂, n₃) ∈ ({(.x, .x, .x), (.x, .y, .y), (.y, .x, .y), (.y, .y, .x)} :
      Finset (Setting × Setting × Setting)))
    (α β γ : ℤˣ) :
    ∫ θ, appendixResponse θ.1 n₁ α * appendixResponse θ.2.1 n₂ β *
        appendixResponse θ.2.2 n₃ γ ∂(appendixDensity n₁ n₂ n₃) =
      bornProb n₁ n₂ n₃ α β γ := 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. 21–22, Appendix 3, Eqs. (39)–(45); discussed on p. 13 around Eq. (33).

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 $n_1,n_2,n_3\in\{x,y\}$ , and assume $(n_1,n_2,n_3)$ is one of $(x,x,x)$ , $(x,y,y)$ , $(y,x,y)$ , $(y,y,x)$ . Then for all $\alpha,\beta,\gamma\in\{\pm1\}$ ,

\int_{\mathbb R^3} r(\theta_1,n_1,\alpha)\,r(\theta_2,n_2,\beta)\,r(\theta_3,n_3,\gamma)\,d\mu_{n_1n_2n_3}(\theta)=\mathrm{bornProb}(n_1,n_2,n_3;\alpha,\beta,\gamma).

The ingredients are:

$r(\theta,x,\alpha)=(1+\alpha\cos\theta)/2$ and $r(\theta,y,\alpha)=(1+\alpha\sin\theta)/2$ ;
$\mu_{n_1n_2n_3}=\frac14\sum\delta_{(\vartheta(n_1,v_1),\vartheta(n_2,v_2),\vartheta(n_3,v_3))}$ , summed over the $(v_1,v_2,v_3)\in\{\pm1\}^3$ with $v_1v_2v_3=s(n_1,n_2,n_3)$ ;
$s(x,x,x)=-1$ , and $s=+1$ otherwise;
$\vartheta(x,1)=0$ , $\vartheta(x,-1)=\pi$ , $\vartheta(y,1)=\pi/2$ , $\vartheta(y,-1)=-\pi/2$ .

The integral is a Bochner integral against a finite sum of point masses. The right-hand side is the Born probability for $\psi=(|000\rangle-|111\rangle)/\sqrt2$ . The other four setting triples are excluded by the membership hypothesis.

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