Time reversal ( $\rho\mapsto\rho^T$ ) is a positive map

Proved

PeresTerno.transpose_isPositiveMap

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

quantum-information

For every finite index set $d$ , the transposition map $\rho\mapsto\rho^{T}$ on complex $d\times d$ matrices is positive: if $\rho$ is positive semidefinite then so is $\rho^{T}$ .

The source states this for complex conjugation of $\rho$ , interpreted as time reversal; on Hermitian matrices complex conjugation and transposition coincide.

Formalization Note Time reversal is encoded as the $\mathbb C$ -linear transposition map, which agrees with entrywise complex conjugation on every Hermitian matrix. The linear form is the one for which complete positivity (next milestone) is meaningful.

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder

Formal statement

namespace PeresTerno

theorem transpose_isPositiveMap {d : Type*} [Fintype d] :
    IsPositiveMap (fun ρ : Matrix d d ℂ => ρᵀ) := 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, "complex conjugation of rho (whose meaning is time reversal) is a positive map"

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.

For every finite index type $d$ , the map sending a complex $d\times d$ matrix $\rho$ to its transpose $\rho^{T}$ (entries $(\rho^T)_{ij} = \rho_{ji}$ , no complex conjugation) is positive: whenever $\rho$ is positive semidefinite, $\rho^{T}$ is 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 a positive map

Time reversal ( $\rho\mapsto\rho^T$ ) is a positive map