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.
choi_iff_posSemidefHere 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.
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.
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.
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.
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.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.