LF2/ChoiConverse: Choi's theorem, the converse direction (PSD Choi ⇒ Kraus)

Category: 2-LF2 (the operational / Born layer).

Glossary: https://glossary.constraintsurfacedynamics.com/choi-theorem/ Plain-language, CSD-role and formal statements of Choi's theorem, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

LF2/QuantumChannel.lean proves the easy direction of Choi's theorem: a Kraus-form channel has a positive-semidefinite Choi matrix (choiMatrix_posSemidef) — the Choi–Jamiołkowski witness of complete positivity. This module proves the converse: every PSD matrix on the composite index Fin M × Fin N is the Choi matrix of some Kraus family. Together they close Choi's theorem: a matrix is a valid Choi matrix iff it is positive semidefinite (choi_iff_posSemidef), i.e. the CP maps Fin N → Fin M are exactly the PSD Choi matrices.

The construction is the spectral one. A PSD Choi matrix C = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| with λᵢ ≥ 0 (Hermitian spectral theorem, eq_eigen_outer, reusing MixedEnsembleIx.outerProduct); the i-th Kraus operator is the eigenvector eᵢ scaled by √λᵢ and uncurried from a vector on Fin M × Fin N to a matrix Fin M ← Fin N (krausOfChoi). Because the Choi matrix is indexed by the product Fin M × Fin N, this "vectorisation / reshape iso" is definitional — an eigenvector already is the data of a Kraus operator — so the content is entirely the √λᵢ · √λᵢ = λᵢ bookkeeping.

Main results

• choiOfKraus — the Choi matrix of a bare Kraus family (no trace-preservation constraint), agreeing with QuantumChannel.choiMatrix on channels (choiMatrix_eq).
• IsHermitian.eq_eigen_outer — the entrywise spectral decomposition C = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| of a Hermitian matrix (the bare-matrix generalisation of DensityOperatorIx.eq_eigen_ensemble).
• krausOfChoi + choiOfKraus_krausOfChoi — the converse: from a PSD C, the family Kᵢ = √λᵢ · unvec(eᵢ) reconstructs C as its Choi matrix.
• choi_iff_posSemidef — Choi's theorem: C is a Choi matrix of some Kraus family iff C is positive semidefinite.

Trace preservation (∑ₖ Kₖ† Kₖ = 1) is the orthogonal condition distinguishing a channel from a general CP map; it corresponds to the partial trace of C over the output index being the identity, and is not imposed here (this is the complete-positivity converse).

References: LF2/QuantumChannel.lean (choiMatrix, choiMatrix_posSemidef, the easy direction); LF2/MixedEnsembleIx.lean (outerProduct, eq_eigen_ensemble — the spectral idiom this reuses); specs/BACKLOG.md (M-tier "Choi converse"); specs/future-work.md.

noncomputable def CSD.LF2.choiOfKraus {ι : Type u_1} [Fintype ι] {N M : ℕ} (kraus : ι → Matrix (Fin M) (Fin N) ℂ) : Matrix (Fin M × Fin N) (Fin M × Fin N) ℂ

The Choi matrix of a bare Kraus family (no trace-preservation constraint): C (m,n)(m',n') = ∑ₖ Kₖ(m,n) · conj(Kₖ(m',n')). This is QuantumChannel.choiMatrix detached from the QuantumChannel bundle, so the converse can quantify over Kraus families without carrying the channel's trace-preservation hypothesis.

Equations

• CSD.LF2.choiOfKraus kraus = ∑ k : ι, Matrix.vecMulVec (fun (p : Fin M × Fin N) => kraus k p.1 p.2) (star fun (p : Fin M × Fin N) => kraus k p.1 p.2)

@[simp]

theorem CSD.LF2.choiOfKraus_apply {ι : Type u_1} [Fintype ι] {N M : ℕ} (kraus : ι → Matrix (Fin M) (Fin N) ℂ) (p q : Fin M × Fin N) : choiOfKraus kraus p q = ∑ k : ι, kraus k p.1 p.2 * star (kraus k q.1 q.2)

theorem CSD.LF2.QuantumChannel.choiMatrix_eq {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : Φ.choiMatrix = choiOfKraus Φ.kraus

QuantumChannel.choiMatrix is choiOfKraus of the channel's Kraus family.

theorem CSD.LF2.choiOfKraus_posSemidef {ι : Type u_1} [Fintype ι] {N M : ℕ} (kraus : ι → Matrix (Fin M) (Fin N) ℂ) : (choiOfKraus kraus).PosSemidef

A bare Kraus family always has a PSD Choi matrix (the easy direction, stated for choiOfKraus). Each vec(Kₖ) vec(Kₖ)† is a rank-one PSD outer product; PSD is closed under sums.

theorem CSD.LF2.IsHermitian.eq_eigen_outer {n : Type u_2} [Fintype n] [DecidableEq n] {C : Matrix n n ℂ} (hC : C.IsHermitian) : C = ∑ i : n, ↑(hC.eigenvalues i) • DensityOperatorIx.outerProduct (hC.eigenvectorBasis i)

Entrywise spectral decomposition of a Hermitian matrix as an eigenvalue-weighted sum of rank-one eigenvector projectors: C = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ|. The bare-matrix generalisation of DensityOperatorIx.eq_eigen_ensemble (identical proof: the Hermitian spectral theorem in diagonalised form, expanded entrywise).

noncomputable def CSD.LF2.krausOfChoi {N M : ℕ} {C : Matrix (Fin M × Fin N) (Fin M × Fin N) ℂ} (hC : C.PosSemidef) : Fin M × Fin N → Matrix (Fin M) (Fin N) ℂ

The reconstructed Kraus family of a PSD Choi matrix. The i-th operator is the i-th eigenvector eᵢ of C scaled by √λᵢ and uncurried into a matrix: since eᵢ is a vector on Fin M × Fin N, Kᵢ m n = √λᵢ · eᵢ(m,n) is exactly its reshape into a Kraus operator Fin M ← Fin N.

Equations

• CSD.LF2.krausOfChoi hC i m n = ↑√(⋯.eigenvalues i) * (⋯.eigenvectorBasis i).ofLp (m, n)

theorem CSD.LF2.choiOfKraus_krausOfChoi {N M : ℕ} {C : Matrix (Fin M × Fin N) (Fin M × Fin N) ℂ} (hC : C.PosSemidef) : choiOfKraus (krausOfChoi hC) = C

Choi's theorem, converse direction: the reconstructed Kraus family krausOfChoi hC has Choi matrix exactly C. So every PSD matrix on Fin M × Fin N is the Choi matrix of a Kraus family — a completely positive map is realised by its PSD Choi witness. The i-th term contributes (√λᵢ · eᵢ(p))·conj(√λᵢ · eᵢ(q)) = λᵢ · eᵢ(p)·conj(eᵢ(q)), matching the i-th term λᵢ |eᵢ⟩⟨eᵢ| of the spectral decomposition.

theorem CSD.LF2.choi_iff_posSemidef {N M : ℕ} (C : Matrix (Fin M × Fin N) (Fin M × Fin N) ℂ) : (∃ (ι : Type) (x : Fintype ι) (kraus : ι → Matrix (Fin M) (Fin N) ℂ), choiOfKraus kraus = C) ↔ C.PosSemidef

Choi's theorem (finite dimensions). A matrix C on the composite index Fin M × Fin N is the Choi matrix of some Kraus family — equivalently, is the Choi–Jamiołkowski image of some completely positive map Fin N → Fin M — iff it is positive semidefinite. The forward direction is choiOfKraus_posSemidef; the converse is choiOfKraus_krausOfChoi, which additionally exhibits the Kraus family explicitly.