Prove2Me

p. 2 — entanglement grows monotonically as ΔϕLR+ΔϕRL\Delta\phi_{LR}+\Delta\phi_{RL} goes from 00 to π\pi, maximal at π\pi

Open
BoseGIE.reducedPurity_strictAnti

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 let ρ1=Tr⁡2∣ψEnd⟩⟨ψEnd∣\rho_1=\operatorname{Tr}_2|\psi_{\mathrm{End}}\rangle\langle\psi_{\mathrm{End}}| be the reduced state of mass 1. Then (i) if 0≤α+β<α′+β′≤π0\le\alpha+\beta<\alpha'+\beta'\le\pi, the purity satisfies Tr⁡ρ1(α′,β′)2<Tr⁡ρ1(α,β)2\operatorname{Tr}\rho_1(\alpha',\beta')^2<\operatorname{Tr}\rho_1(\alpha,\beta)^2; and (ii) if α+β=π\alpha+\beta=\pi then ρ1=121\rho_1=\tfrac12\mathbb 1 (maximally mixed, so ψEnd\psi_{\mathrm{End}} is maximally entangled).

Formalization Note The source names no entanglement measure. For pure two-qubit states every standard measure is a monotone function of the reduced-state purity, which is used here.

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 reducedPurity_strictAnti :
    (∀ α β α' β' : ℝ, 0 ≤ α + β → α + β < α' + β' → α' + β' ≤ Real.pi →
        reducedPurity (psiEnd α' β') < reducedPurity (psiEnd α β)) ∧
    (∀ α β : ℝ, α + β = Real.pi → ptrace₂ (pureDM (psiEnd α β)) = (1 / 2 : ℂ) • 1) := 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

Notation: for real α,β\alpha,\beta, ψ(α,β)\psi(\alpha,\beta) is 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). ρ=∣ψ⟩⟨ψ∣\rho=|\psi\rangle\langle\psi| has entries ρ(j,k),(j′,k′)=ψjkψj′k′‾\rho_{(j,k),(j',k')}=\psi_{jk}\overline{\psi_{j'k'}}. Tr2ρ\mathrm{Tr}_2\rho is the 2×22\times2 matrix (Tr2ρ)jj′=∑kρ(j,k),(j′,k)(\mathrm{Tr}_2\rho)_{jj'}=\sum_k\rho_{(j,k),(j',k)}. The purity is P(α,β)=Re Tr[(Tr2ρ)2]P(\alpha,\beta)=\mathrm{Re}\,\mathrm{Tr}\big[(\mathrm{Tr}_2\rho)^2\big].

The theorem is a conjunction of two statements.

(a) For all real α,β,α′,β′\alpha,\beta,\alpha',\beta' satisfying

0≤α+β<α′+β′≤π,0\le \alpha+\beta<\alpha'+\beta'\le\pi,

we have P(α′,β′)<P(α,β)P(\alpha',\beta')<P(\alpha,\beta). (Strict inequality; the hypotheses constrain only the sums, with the left endpoint 00 included and the right endpoint π\pi included.)

(b) For all real α,β\alpha,\beta with α+β=π\alpha+\beta=\pi,

Tr2(∣ψ(α,β)⟩⟨ψ(α,β)∣)=12 12,\mathrm{Tr}_2\big(|\psi(\alpha,\beta)\rangle\langle\psi(\alpha,\beta)|\big)=\tfrac12\,\mathbb 1_{2},

the 2×22\times2 identity matrix times 12\tfrac12.

Both parts are universally quantified over reals, with no further parameters; the hypotheses are satisfiable, so neither part is vacuous.

View graph