Two masses as orbital qubits: the evolved state, product vectors, separability and reduced purity (Bose et al. 2017)

Definition

BoseGIE_defs

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

entanglementgravitationally-induced-entanglementquantum-gravityquantum-information

Shared vocabulary of the mission. Each mass is an orbital qubit ( $0=|L\rangle$ , $1=|R\rangle$ ); two-qubit objects are indexed by pairs $(j,k)$ with mass 1 first. Defines the evolved state $\psi_{\mathrm{End}}(\alpha,\beta)=\tfrac12(|LL\rangle+e^{i\alpha}|LR\rangle+e^{i\beta}|RL\rangle+|RR\rangle)$ (Eq. (2), global phase omitted); product vectors $u\otimes w$ ; the projector $|v\rangle\langle v|$ ; the partial trace over mass 2 and the reduced-state purity $\operatorname{Tr}\rho_1^2$ ; and separable states: finite convex combinations $\sum_i p_i\,\rho_i^{(1)}\otimes\rho_i^{(2)}$ of products of density matrices (PeresTerno.IsDensityMatrix: PSD, trace one).

Definition code

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

/-!
# Gravitationally induced entanglement of two masses

Definitions for the mission drafted from S. Bose, A. Mazumdar, G. W. Morley, H. Ulbricht,
M. Toroš, M. Paternostro, A. A. Geraci, P. F. Barker, M. S. Kim and G. Milburn,
*A Spin Entanglement Witness for Quantum Gravity*, Phys. Rev. Lett. 119, 240401 (2017),
arXiv:1707.06050v1, p. 2, Eqs. (1)–(2).

Each test mass `j = 1, 2` is an "orbital qubit" with basis `|L⟩, |R⟩` (or, on p. 3, the
spin-orbital states `|L,↑⟩, |R,↓⟩`), encoded as `Fin 2` with `0 ↦ |L⟩` and `1 ↦ |R⟩`.
Two-qubit vectors and matrices are indexed by `Qubit × Qubit`, the first component being mass 1.
-/

namespace BoseGIE

open Matrix
open scoped Kronecker ComplexOrder

noncomputable section

/-- An orbital qubit: `0 ↦ |L⟩`, `1 ↦ |R⟩`. -/
abbrev Qubit := Fin 2

/-- Eq. (2), global phase `e^{iφ}` omitted: the two-qubit state
`½ (|LL⟩ + e^{iΔφ_LR} |LR⟩ + e^{iΔφ_RL} |RL⟩ + |RR⟩)`, with `α = Δφ_LR` and `β = Δφ_RL`.
The entry at `(j, k)` is the amplitude of mass 1 in `j` and mass 2 in `k`. -/
def psiEnd (α β : ℝ) : Qubit × Qubit → ℂ :=
  fun p => (1 / 2 : ℂ) *
    (!![1, Complex.exp (α * Complex.I); Complex.exp (β * Complex.I), 1] : Matrix Qubit Qubit ℂ)
      p.1 p.2

/-- A two-qubit vector factorizes as `u ⊗ w`. -/
def IsProductVector (v : Qubit × Qubit → ℂ) : Prop :=
  ∃ u w : Qubit → ℂ, ∀ i j, v (i, j) = u i * w j

/-- The density matrix `|v⟩⟨v|` of a vector `v`. -/
def pureDM (v : Qubit × Qubit → ℂ) : Matrix (Qubit × Qubit) (Qubit × Qubit) ℂ :=
  Matrix.of fun p q => v p * star (v q)

/-- Partial trace over mass 2: `(Tr₂ ρ)_{ij} = ∑ₖ ρ_{(i,k),(j,k)}` (the reduced state of mass 1). -/
def ptrace₂ (ρ : Matrix (Qubit × Qubit) (Qubit × Qubit) ℂ) : Matrix Qubit Qubit ℂ :=
  Matrix.of fun i j => ∑ k, ρ (i, k) (j, k)

/-- The purity `Tr ρ₁²` of the reduced state `ρ₁ = Tr₂ |v⟩⟨v|` of mass 1 (real part). -/
def reducedPurity (v : Qubit × Qubit → ℂ) : ℝ :=
  (ptrace₂ (pureDM v) * ptrace₂ (pureDM v)).trace.re

/-- Separable two-qubit state: a finite convex combination `∑ᵢ pᵢ ρᵢ^{(1)} ⊗ ρᵢ^{(2)}` of
products of density matrices. A state is entangled when it is not separable. -/
def IsSeparable (ρ : Matrix (Qubit × Qubit) (Qubit × Qubit) ℂ) : Prop :=
  ∃ (n : ℕ) (p : Fin n → ℝ) (ρ₁ ρ₂ : Fin n → Matrix Qubit Qubit ℂ),
    (∀ i, 0 ≤ p i) ∧ ∑ i, p i = 1 ∧
    (∀ i, PeresTerno.IsDensityMatrix (ρ₁ i)) ∧ (∀ i, PeresTerno.IsDensityMatrix (ρ₂ i)) ∧
    ρ = ∑ i, (p i : ℂ) • (ρ₁ i ⊗ₖ ρ₂ i)

end

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, Eqs. (1)–(2)

Read-back

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

Let $Q=\{0,1\}$ (a "qubit" index set). Two-qubit vectors are functions $Q\times Q\to\mathbb C$ and two-qubit matrices are indexed by pairs in $Q\times Q$ ; the first component of a pair is "mass 1", the second is "mass 2".

psiEnd. For real $\alpha,\beta$ , $\psi(\alpha,\beta)$ is the vector with $\psi_{(j,k)}=\tfrac12 M_{jk}$ , where $M=\begin{pmatrix}1 & e^{i\alpha}\\ e^{i\beta} & 1\end{pmatrix}$ (row $j$ = mass 1, column $k$ = mass 2). So $\psi_{00}=\psi_{11}=\tfrac12$ , $\psi_{01}=\tfrac12 e^{i\alpha}$ , $\psi_{10}=\tfrac12 e^{i\beta}$ .

IsProductVector. $v$ is a product vector iff there exist $u,w:Q\to\mathbb C$ with $v_{(i,j)}=u_i w_j$ for all $i,j$ (the zero vector counts as a product).

pureDM. $\mathrm{pureDM}(v)_{p,q}=v_p\,\overline{v_q}$ , i.e. $|v\rangle\langle v|$ , with no normalization.

ptrace₂. For a $4\times4$ matrix $\rho$ , $(\mathrm{Tr}_2\rho)_{ij}=\sum_{k\in Q}\rho_{(i,k),(j,k)}$ , a $2\times2$ matrix (traces out the second factor).

reducedPurity. $\mathrm{reducedPurity}(v)=\mathrm{Re}\,\mathrm{Tr}\big[(\mathrm{Tr}_2|v\rangle\langle v|)^2\big]\in\mathbb R$ . No normalization of $v$ is imposed.

IsSeparable. A $4\times4$ matrix $\rho$ is separable iff there exist $n\in\mathbb N$ , reals $p_1,\dots,p_n\ge0$ with $\sum p_i=1$ , and $2\times2$ matrices $\rho^{(1)}_i,\rho^{(2)}_i$ , each positive semidefinite with trace $1$ (PosSemidef and trace $=1$ , as in PeresTerno.IsDensityMatrix), such that

\rho=\sum_{i=1}^n p_i\,\rho^{(1)}_i\otimes\rho^{(2)}_i,

with the Kronecker product $(A\otimes B)_{(i,k),(j,l)}=A_{ij}B_{kl}$ (first factor = mass 1). Since $\sum p_i=1$ , $n=0$ is impossible, so $n\ge1$ .

View graph