Eq. (6) is a completely positive map

Proved

PeresTerno.krausUpdate_completelyPositive

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

quantum-information

Let $\{A_m\}_{m\in I}$ be a finite family of complex $e\times d$ matrices and let $T(\rho) = \sum_m A_m\rho A_m^\dagger$ . Then $T$ is completely positive: for every $n\in\mathbb N$ and every positive semidefinite matrix $R$ on $\mathbb C^d\otimes\mathbb C^n$ , the matrix $(T\otimes\mathbb 1_n)(R)$ is positive semidefinite.

This is the "Kraus maps are completely positive" half of the source's statement that Eq. (6) is the most general completely positive linear map.

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder

Formal statement

namespace PeresTerno

theorem krausUpdate_completelyPositive {d e ι : Type*} [Fintype d] [Fintype e] [Fintype ι]
    (A : ι → Matrix e d ℂ) :
    IsCompletelyPositive (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, paragraph after Eq. (6) ("Eq. (6) is the most general completely positive linear 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 finite index types $d$ , $e$ , $I$ and every family $A : I\to\mathbb C^{e\times d}$ , the map $\rho\mapsto\sum_{m\in I}A_m\rho A_m^\dagger$ is completely positive in the sense of the definition file: for every natural number $n$ (including $0$ ) and every positive semidefinite complex matrix $R$ indexed by $d\times\{0,\dots,n-1\}$ , the matrix indexed by $e\times\{0,\dots,n-1\}$ with entries

\Big[\sum_m A_m R^{(a,b)} A_m^\dagger\Big]_{kl}\ \text{ at } ((k,a),(l,b)),\qquad R^{(a,b)}_{ij}=R_{(i,a),(j,b)},

is positive semidefinite. No hypothesis on $A$ .

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