Choi's theorem

A quantum channel is legitimate exactly when one matrix built from it is positive semidefinite -- both directions machine-checked, so "is this map physical" is a decidable linear-algebra question.

proved in corpus · proved here, no imported axiomsLean choi_iff_posSemidef

In plain terms

Here is the problem. Which transformations of a quantum state are physically allowed? The abstract answer -- completely positive trace-preserving maps -- involves a quantifier over all possible bystander systems, which is not something you can check by computation.

Choi's 1975 insight collapses the quantifier: encode the whole map into a single matrix -- feed it half of a maximally entangled pair -- and the map is legitimate precisely when that one matrix is positive semidefinite. An infinite family of conditions becomes one eigenvalue check.

The corpus proves both directions: every Kraus-form channel has a positive Choi matrix, and every positive matrix on the composite index arises from some Kraus family. The equivalence is the theorem.

In CSD

Choi's theorem is the workhorse of the corpus's channel layer: the generator-tier positivity witnesses in the open-system results, the channel constructions of the coarse-graining tier, and the jump-part arguments in the Lindblad complete-positivity proof all route through Kraus decompositions certified by it.

It sits on the operational stratum -- standard quantum information, formalised because the programme's claims lean on it, with the construction fully explicit: the converse direction actually builds the Kraus family from the spectral decomposition of the Choi matrix.

Mathematically

choi_iff_posSemidef: a matrix on the composite index is the Choi matrix of some Kraus family if and only if it is positive semidefinite. The forward direction is the rank-one decomposition of the Choi matrix into outer products of vectorised Kraus operators; the converse reconstructs Kraus operators from a PSD matrix's spectral square roots, de-vectorised along the index pairing.

The name

Man-Duen Choi, born 1945 in Hong Kong, spent his career at the University of Toronto working in operator algebras. The 1975 paper -- Completely positive linear maps on complex matrices, in Linear Algebra and its Applications -- is a model of brevity, and its central object was independently studied by Andrzej Jamiolkowski, which is why the encoding is often called the Choi-Jamiolkowski isomorphism.

Module
CsdLean4/LF2/ChoiConverse.lean
Related
quantum channel, lindblad equation, loewner order

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy