p. 2 — $|\Psi(t=\tau)\rangle$ cannot be factorized when $\Delta\phi_{LR}+\Delta\phi_{RL}\neq 2n\pi$

Open

BoseGIE.psiEnd_not_product

by Alien60 · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

entanglementgravitationally-induced-entanglementquantum-gravityquantum-information

Let $\psi_{\mathrm{End}}(\alpha,\beta)=\tfrac12\big(|LL\rangle+e^{i\alpha}|LR\rangle+e^{i\beta}|RL\rangle+|RR\rangle\big)$ (first factor = mass 1; $\alpha=\Delta\phi_{LR}$ , $\beta=\Delta\phi_{RL}$ ; global phase omitted). If $\alpha+\beta\neq 2n\pi$ for every integer $n$ , then $\psi_{\mathrm{End}}(\alpha,\beta)$ is not a product vector: there are no $u,w\in\mathbb C^2$ with $\psi_{\mathrm{End}}(\alpha,\beta)_{jk}=u_j w_k$ for all $j,k$ .

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics
import Definitions.Def_BoseGIE_defs

open Matrix
open scoped Kronecker ComplexOrder

Formal statement

namespace BoseGIE

theorem psiEnd_not_product (α β : ℝ) (h : ∀ n : ℤ, α + β ≠ 2 * Real.pi * n) :
    ¬ IsProductVector (psiEnd α β) := by sorry

end BoseGIE

Source

S. Bose et al., A Spin Entanglement Witness for Quantum Gravity, Phys. Rev. Lett. 119, 240401 (2017), https://arxiv.org/abs/1707.06050v1, p. 2, paragraph after Eq. (2)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\alpha,\beta\in\mathbb R$ and suppose that for every integer $n\in\mathbb Z$ , $\alpha+\beta\neq 2\pi n$ (i.e. $\alpha+\beta$ is not an integer multiple of $2\pi$ ; equivalently $e^{i(\alpha+\beta)}\ne1$ ).

Let $\psi(\alpha,\beta)$ be the two-qubit vector (indices $j,k\in\{0,1\}$ , first = mass 1) with entries $\psi_{jk}=\tfrac12 M_{jk}$ , $M=\begin{pmatrix}1&e^{i\alpha}\\ e^{i\beta}&1\end{pmatrix}$ .

The theorem states that there do not exist functions $u,w:\{0,1\}\to\mathbb C$ with $\psi_{jk}=u_jw_k$ for all $j,k\in\{0,1\}$ . That is, $\psi(\alpha,\beta)$ is not a product vector.

Only this one direction is asserted: no claim is made about the case $\alpha+\beta\in2\pi\mathbb Z$ . The hypothesis is satisfiable (e.g. $\alpha=\beta=\pi/2$ ), so the statement is not vacuous. The integer is cast to $\mathbb R$ in $2\pi n$ .

View graph

p. 2 — ∣Ψ(t=τ)⟩|\Psi(t=\tau)\rangle∣Ψ(t=τ)⟩ cannot be factorized when ΔϕLR+ΔϕRL≠2nπ\Delta\phi_{LR}+\Delta\phi_{RL}\neq 2n\piΔϕLR​+ΔϕRL​=2nπ

p. 2 — $|\Psi(t=\tau)\rangle$ cannot be factorized when $\Delta\phi_{LR}+\Delta\phi_{RL}\neq 2n\pi$