Eq. (6) is the most general completely positive linear map (Kraus representation)

Proved

PeresTerno.completelyPositive_exists_kraus

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

quantum-information

Let $d$ and $e$ be finite index sets and let $T$ be a $\mathbb C$ -linear map from complex $d\times d$ matrices to complex $e\times e$ matrices. If $T$ is completely positive, then there exist $N\in\mathbb N$ and complex $e\times d$ matrices $A_1,\dots,A_N$ such that

T(\rho) = \sum_{k=1}^{N} A_k\,\rho\,A_k^\dagger \qquad\text{for every } \rho .

Together with the complete positivity of Kraus maps, this is the source's statement that Eq. (6) is the most general completely positive linear map (the Kraus/Choi representation theorem).

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder

Formal statement

namespace PeresTerno

theorem completelyPositive_exists_kraus {d e : Type*} [Fintype d] [Fintype e]
    [DecidableEq d] [DecidableEq e]
    (T : Matrix d d ℂ →ₗ[ℂ] Matrix e e ℂ) (hT : IsCompletelyPositive T) :
    ∃ (N : ℕ) (A : Fin N → Matrix e d ℂ), ∀ ρ, T ρ = krausUpdate A ρ := 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, "Eq. (6) is the most general completely positive linear map (Stinespring, 1955; Davies, 1976; Kraus, 1983)"

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 finite index types $d$ , $e$ (with decidable equality) and every $\mathbb C$ -linear map $T$ from complex $d\times d$ matrices to complex $e\times e$ matrices that is completely positive in the sense of the definition file (for every $n\in\mathbb N$ the blockwise ampliation of $T$ sends positive semidefinite matrices on $d\times\{0,\dots,n-1\}$ to positive semidefinite matrices), there exist a natural number $N$ (possibly $0$ ) and complex $e\times d$ matrices $A_0,\dots,A_{N-1}$ such that for every complex $d\times d$ matrix $\rho$ ,

T(\rho) = \sum_{k=0}^{N-1} A_k\,\rho\,A_k^\dagger .

No bound on $N$ is asserted.

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