Prove2Me

p. 2 — the gravitationally evolved state is entangled iff ΔϕLR+ΔϕRL∉2πZ\Delta\phi_{LR}+\Delta\phi_{RL}\notin 2\pi\mathbb Z

Open
BoseGIE.evolvedState_entangled_iff

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

entanglementgravitationally-induced-entanglementquantum-gravityquantum-information

Let ψEnd(α,β)=12(∣LL⟩+eiα∣LR⟩+eiβ∣RL⟩+∣RR⟩)\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; α=ΔϕLR\alpha=\Delta\phi_{LR}, β=ΔϕRL\beta=\Delta\phi_{RL}; global phase omitted) and ρ=∣ψEnd⟩⟨ψEnd∣\rho=|\psi_{\mathrm{End}}\rangle\langle\psi_{\mathrm{End}}|. Then ρ\rho is entangled, i.e. not separable (not a finite convex combination ∑ipi ρi(1)⊗ρi(2)\sum_i p_i\,\rho_i^{(1)}\otimes\rho_i^{(2)} of products of qubit density matrices), if and only if α+β≠2nπ\alpha+\beta\neq 2n\pi for every integer nn.

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 evolvedState_entangled_iff (α β : ℝ) :
    ¬ IsSeparable (pureDM (psiEnd α β)) ↔ ∀ n : ℤ, α + β ≠ 2 * Real.pi * n := 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): '... cannot be factorized and is thereby in an entangled state of the two orbital qubits'
Read-back

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

For real α,β\alpha,\beta, let ψ(α,β)\psi(\alpha,\beta) be the two-qubit vector with entries ψjk=12(1eiαeiβ1)jk\psi_{jk}=\tfrac12\begin{pmatrix}1&e^{i\alpha}\\ e^{i\beta}&1\end{pmatrix}_{jk} (first index = mass 1), and ρ=∣ψ⟩⟨ψ∣\rho=|\psi\rangle\langle\psi|, i.e. ρp,q=ψpψq‾\rho_{p,q}=\psi_p\overline{\psi_q} (4×44\times4 matrix).

Call a 4×44\times4 matrix separable if it equals ∑i=1npi ρi(1)⊗ρi(2)\sum_{i=1}^n p_i\,\rho^{(1)}_i\otimes\rho^{(2)}_i for some n∈Nn\in\mathbb N, weights pi≥0p_i\ge0 with ∑pi=1\sum p_i=1, and 2×22\times2 matrices ρi(1),ρi(2)\rho^{(1)}_i,\rho^{(2)}_i that are positive semidefinite with trace 11 (Kronecker product, first factor = mass 1).

The theorem: for all real α,β\alpha,\beta,

ρ is not separable  ⟺  ∀n∈Z: α+β≠2πn.\rho\text{ is not separable}\iff \forall n\in\mathbb Z:\ \alpha+\beta\neq2\pi n .

So the state is non-separable exactly when α+β\alpha+\beta is not an integer multiple of 2π2\pi (equivalently ei(α+β)≠1e^{i(\alpha+\beta)}\neq1); and, in the other direction, when α+β∈2πZ\alpha+\beta\in2\pi\mathbb Z the matrix ρ\rho is separable. Both directions are asserted. The integer nn is cast to R\mathbb R.

View graph