Time reversal ( $\rho\mapsto\rho^T$ ) is not completely positive

Proved

PeresTerno.transpose_not_completelyPositive

by Lucas · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-information

The transposition map $\rho\mapsto\rho^{T}$ on complex $2\times 2$ matrices is not completely positive: there are $n\in\mathbb N$ and a positive semidefinite matrix $R$ on $\mathbb C^2\otimes\mathbb C^n$ such that applying the transposition to each $2\times 2$ block of $R$ (the partial transpose) yields a matrix that is not positive semidefinite.

This is the source's remark that time reversal applied to only one of two systems produces an unphysical "density matrix" with negative eigenvalues.

Formalization Note Stated for a qubit; this suffices to show that time reversal is not completely positive in general.

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder

Formal statement

namespace PeresTerno

theorem transpose_not_completelyPositive :
    ¬ IsCompletelyPositive (fun ρ : Matrix (Fin 2) (Fin 2) ℂ => ρᵀ) := by
  sorry

end PeresTerno

Source

A. Peres and D. R. Terno, Quantum information and relativity theory, Rev. Mod. Phys. 76, 93-123 (2004), https://doi.org/10.1103/RevModPhys.76.93, p. 100, Sec. II.D, "However, it is not completely positive"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - NON-BLIND: same agent that drafted the statements

Non-blind read-back - not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning, at the explicit request of the proposal owner. It was not produced by a blind, independent auditor and must not be mistaken for independent testimony. Reviewers should compare the Lean code against the source themselves.

It is not the case that the transposition map on complex $2\times 2$ matrices is completely positive in the sense of the definition file. Equivalently: there exist a natural number $n$ and a positive semidefinite complex matrix $R$ indexed by $\{0,1\}\times\{0,\dots,n-1\}$ such that the matrix with entry $R_{(j,a),(i,b)}$ at row $(i,a)$ , column $(j,b)$ (each $2\times 2$ block transposed) is not positive semidefinite.

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Time reversal (ρ↦ρT\rho\mapsto\rho^Tρ↦ρT) is not completely positive

Time reversal ( $\rho\mapsto\rho^T$ ) is not completely positive