Formalize Open Quantum Problem #18: Qubit bi-negativity

### What is the conjecture

This is problem [#18](https://oqp.iqoqi.oeaw.ac.at/qubit-bi-negativity) in [Reinhard F. Werner's collection](https://arxiv.org/abs/quant-ph/0504166), later [collected by a community of quantum researchers](https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems).

**Status:** this problem is listed as **solved** on the [Solved Quantum Problems](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems) page (solved by S. Ishizaka, 2004; see below).

> **Problem (Open Quantum Problem #18: “Qubit bi-negativity”).**
> Prove that
> `|σ^{T_2}|^{T_2} ≥ 0`
> holds for every two-qubit state `σ`. Here, `T_2` denotes the partial transpose with respect to the second system, and `|X|` is the operator absolute value.

Concretely, let `σ` be a density operator on `C^2 ⊗ C^2`, and let `T_2 = id ⊗ T` be partial transpose on the second tensor factor (in a fixed product basis). For any operator `X`, write `|X| = (X^† X)^{1/2}`; since `σ^{T_2}` is Hermitian, this is equivalently `|σ^{T_2}| = ((σ^{T_2})^2)^{1/2}`.

The bi-negativity question asks whether the operator obtained by partial transposition, absolute value, and partial transposition again is always positive semidefinite for two qubits. This operator is usually called the **bi-negativity** or **binegativity** of `σ`.

A useful reformulation for formalization is that, for an entangled two-qubit state, `σ^{T_2}` has exactly one negative eigenvalue, so it can be written as
`σ^{T_2} = P - λ |ψ⟩⟨ψ|`,
with `P ≥ 0`, `λ > 0`, and `P|ψ⟩ = 0`.
Then
`|σ^{T_2}|^{T_2} = 2 P^{T_2} - σ`.

**Solved statement to formalize (Ishizaka, 2004):**
For every two-qubit state `σ`, one has
`|σ^{T_2}|^{T_2} ≥ 0`.

Ishizaka first proves a stronger structural theorem: if `P` denotes the positive part of `σ^{T_2}`, then `P` is PPT, i.e. `P^{T_2} ≥ 0`; if `σ` is entangled, then `P^{T_2}` is full rank. In `2 ⊗ 2`, PPT is equivalent to separability, so this gives a separable approximation to the entangled state and is a key step in the proof.

**Important caveat:** this is a genuinely `2 ⊗ 2` statement. The same positivity property does **not** hold in general in higher dimensions; the literature refers to counterexamples as **binegative states**, and Ishizaka reports such examples numerically already in `3 ⊗ 3`.

### Where to find the details / references

Primary sources:
- [Open Quantum Problems site (Problem #18)](https://oqp.iqoqi.oeaw.ac.at/qubit-bi-negativity)
- [Solved Quantum Problems list (shows #18 solved)](https://oqp.iqoqi.oeaw.ac.at/solved-quantum-problems)
- [Werner / Krüger–Werner arXiv list](https://arxiv.org/abs/quant-ph/0504166) (see “Problem 18”)

Key solution reference (as cited on the OQP page):
- S. Ishizaka, **“Binegativity and geometry of entangled states in two qubits”**, *Phys. Rev. A* 69, 020301(R) (2004); arXiv: [quant-ph/0308056](https://arxiv.org/abs/quant-ph/0308056)

Original source of the problem (as cited on the OQP page):
- K. Audenaert, B. De Moor, K. G. H. Vollbrecht, and R. F. Werner, **“Asymptotic Relative Entropy of Entanglement for Orthogonally Invariant States”**, *Phys. Rev. A* 66, 032310 (2002); arXiv: [quant-ph/0204143](https://arxiv.org/abs/quant-ph/0204143)

Useful background / motivation:
- K. Audenaert, M. B. Plenio, and J. Eisert, **“The entanglement cost under operations preserving the positivity of partial transpose”**, *Phys. Rev. Lett.* 90, 027901 (2003); arXiv: [quant-ph/0207146](https://arxiv.org/abs/quant-ph/0207146)
- A. Peres, **“Separability Criterion for Density Matrices”**, *Phys. Rev. Lett.* 77, 1413 (1996)
- M. Horodecki, P. Horodecki, and R. Horodecki, **“Separability of mixed states: necessary and sufficient conditions”**, *Phys. Lett. A* 223, 1 (1996)

### Prerequisites needed

- Two-qubit density operators on `C^2 ⊗ C^2`; tensor products; adjoints; traces
- Partial transpose / PPT criterion, especially the fact that in `2 ⊗ 2` one has PPT `⇔` separable
- Spectral decomposition of Hermitian operators; positive/negative parts; operator absolute value
- Basic matrix analysis: positivity, eigenvalues, rank, full rank
- (If following Ishizaka’s proof) Bell-basis representations and local filtering / normal forms for two-qubit states
- Entanglement witnesses and their relation to partial transpose

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

- ams-81 (Quantum theory)
- ams-15 (Linear and multilinear algebra; matrix theory)
- ams-47 (Operator theory)

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [X] This issue is up for grabs: I would like to see this conjecture added by somebody else
---

No repository file, test, or entry point is named. Start with Ishizaka’s cited solution and the stated prerequisites, then identify the relevant existing formalizations; done means a Lean formalization proving |σ^{T_2}|^{T_2} ≥ 0 for every two-qubit state σ.

Written by the indexing model from the issue text.