p. 3 — the spin entanglement witness: $\mathcal W\le 1$ on every separable two-qubit state

Proved

BMV2017.witness_le_one_of_separable

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

entanglement-witnessgravitationally-induced-entanglementquantum-gravityquantum-information

Let $\rho$ be a separable two-qubit state: $\rho=\sum_{i=1}^n p_i\,\rho_i^{(1)}\otimes\rho_i^{(2)}$ with $p_i\ge0$ , $\sum_ip_i=1$ and $\rho_i^{(1)},\rho_i^{(2)}$ qubit density matrices. Then

\mathcal W(\rho)=\big|\operatorname{Tr}\rho(\sigma_x\otimes\sigma_z)-\operatorname{Tr}\rho(\sigma_y\otimes\sigma_y)\big|\le 1 .

Equivalently, $\mathcal W(\rho)>1$ certifies that $\rho$ is entangled.

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics
import Definitions.Def_BMV2017_defs

open Matrix
open scoped Kronecker ComplexOrder

Formal statement

namespace BMV2017

theorem witness_le_one_of_separable (ρ : Matrix (Qubit × Qubit) (Qubit × Qubit) ℂ)
    (hρ : IsSeparable ρ) : witness ρ ≤ 1 := by sorry

end BMV2017

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. 3: 'W = |⟨σx(1)⊗σz(2)⟩ − ⟨σy(1)⊗σy(2)⟩|. If W is found to exceed unity then the state is proven to be entangled'

Read-back

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

Setting. A qubit index is an element of $\{0,1\}$ . Two-qubit matrices are $4\times 4$ complex matrices whose rows and columns are indexed by ordered pairs $(i,k)\in\{0,1\}\times\{0,1\}$ ; the first component $i$ is called "factor 1" and the second component $k$ "factor 2". For $2\times 2$ complex matrices $A,B$ , the Kronecker product $A\otimes B$ is the two-qubit matrix with entries

(A\otimes B)_{(i,k),(j,l)} = A_{ij}\,B_{kl},

so $A$ acts on factor 1 (first component) and $B$ on factor 2 (second component).

Binders and hypothesis. The theorem quantifies over a single object: an arbitrary two-qubit complex matrix $\rho$ (no Hermiticity, positivity or trace condition is imposed on $\rho$ directly). Its only hypothesis is that $\rho$ is separable in the following sense: there exist

a natural number $n$ ,
real numbers $p_0,\dots,p_{n-1}$ ,
$2\times 2$ complex matrices $\rho^{(1)}_0,\dots,\rho^{(1)}_{n-1}$ and $\rho^{(2)}_0,\dots,\rho^{(2)}_{n-1}$ ,

such that

$p_i \ge 0$ for every $i$ ;
$\sum_{i=0}^{n-1} p_i = 1$ ;
every $\rho^{(1)}_i$ is a density matrix;
every $\rho^{(2)}_i$ is a density matrix;
$\displaystyle \rho = \sum_{i=0}^{n-1} p_i\,\bigl(\rho^{(1)}_i \otimes \rho^{(2)}_i\bigr)$ (with $p_i$ viewed as a complex scalar), exact matrix equality.

Here a $2\times 2$ complex matrix $\sigma$ is a density matrix when it is positive semidefinite — i.e. Hermitian ( $\sigma^\dagger=\sigma$ ) and $v^\dagger \sigma v$ is a nonnegative real number for every $v\in\mathbb{C}^2$ — and its trace equals $1$ (as a complex number).

Edge cases of the hypothesis. The case $n=0$ is excluded automatically: the empty sum of the $p_i$ is $0\neq 1$ , so condition 2 forces $n\ge 1$ . Weights $p_i=0$ are allowed, and the factors $\rho^{(1)}_i,\rho^{(2)}_i$ need not be distinct, pure, or related across $i$ . The hypothesis is satisfiable (e.g. $n=1$ , $p_0=1$ , $\rho^{(1)}_0=\rho^{(2)}_0=\operatorname{diag}(1,0)$ ). Any $\rho$ satisfying it is in particular Hermitian, positive semidefinite and of trace $1$ , but this is a consequence, not an extra assumption.

The witness. With the Pauli matrices

\sigma_x=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad \sigma_y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix},\qquad \sigma_z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}

(row/column index $0$ first), the quantity $\mathcal W(\rho)$ is the real number

\mathcal W(\rho) = \Bigl|\,\operatorname{Tr}\bigl(\rho\,(\sigma_x\otimes\sigma_z)\bigr) - \operatorname{Tr}\bigl(\rho\,(\sigma_y\otimes\sigma_y)\bigr)\Bigr|,

where $\operatorname{Tr}$ is the ordinary matrix trace (sum of the four diagonal entries) of the $4\times 4$ product $\rho\cdot O$ (with $\rho$ on the left), the two traces are complex numbers, and $|\cdot|$ is the complex modulus of their difference (not the real part or the absolute value of the real part). In the first operator, $\sigma_x$ sits on factor 1 and $\sigma_z$ on factor 2; the second operator has $\sigma_y$ on both factors.

Conclusion. For every two-qubit complex matrix $\rho$ that is separable in the above sense,

\mathcal W(\rho) \le 1,

a non-strict inequality between real numbers. The theorem asserts only this upper bound; it makes no claim about attainment of the value $1$ , about non-separable matrices, or about any converse.

View graph

p. 3 — the spin entanglement witness: W≤1\mathcal W\le 1W≤1 on every separable two-qubit state

p. 3 — the spin entanglement witness: $\mathcal W\le 1$ on every separable two-qubit state