LF2/QuantumChannel: quantum channels (CPTP maps) — Kraus form + CPTP-forward (tranche 1)

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

Glossary: https://glossary.constraintsurfacedynamics.com/quantum-channel/ Plain-language, CSD-role and formal statements of quantum channels, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The general open-system dynamics pillar: a quantum channel is a completely-positive trace-preserving (CPTP) map on density operators. We take the operational Kraus definition — a finite family of operators Kₖ with ∑ₖ Kₖ† Kₖ = 1 — and prove the CPTP-forward content: a channel maps density operators to density operators (this tranche). Later tranches add the Stinespring dilation and the Choi matrix.

• QuantumChannel ι N M — a Kraus family kraus : ι → Matrix (Fin M) (Fin N) ℂ with the trace-preservation constraint ∑ₖ Kₖ† Kₖ = 1;
• apply Φ ρ = ∑ₖ Kₖ ρ Kₖ† — the channel action, and channelApply its action on DensityOperators;
• apply_posSemidef / apply_trace — positivity and trace preservation, so channelApply lands in DensityOperator M (the CPTP-forward theorem);
• unitaryChannel — unitary conjugation ρ ↦ U ρ U† is a channel (closed dynamics as a special case);
• comp — channels compose (κ × ι Kraus family), so the channels form a composition monoid.

Built on LF2.DensityOperator and Mathlib's Matrix.PosSemidef.mul_mul_conjTranspose_same, Matrix.posSemidef_sum, Matrix.trace_mul_comm.

References: LF2/BornWrapper.lean (DensityOperator, traceForm); LF2/ReducedDensity.lean (partialTrace*, for the forthcoming Stinespring tranche); specs/future-work.md.

structure CSD.LF2.QuantumChannel (ι : Type u_3) [Fintype ι] (N M : ℕ) : Type u_3

A quantum channel in Kraus form. A finite family of Kraus operators Kₖ : Fin M ← Fin N with the trace-preservation constraint ∑ₖ Kₖ† Kₖ = 1. The operational definition of a CPTP map from an N-dimensional to an M-dimensional system.

• kraus : ι → Matrix (Fin M) (Fin N) ℂ

  The Kraus operators.

• isTracePreserving : ∑ k : ι, (self.kraus k).conjTranspose * self.kraus k = 1

  Trace preservation: ∑ₖ Kₖ† Kₖ = 1.

noncomputable def CSD.LF2.QuantumChannel.apply {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (ρ : Matrix (Fin N) (Fin N) ℂ) : Matrix (Fin M) (Fin M) ℂ

The channel action Φ(ρ) = ∑ₖ Kₖ ρ Kₖ†.

Equations

• Φ.apply ρ = ∑ k : ι, Φ.kraus k * ρ * (Φ.kraus k).conjTranspose

theorem CSD.LF2.QuantumChannel.apply_posSemidef {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) {ρ : Matrix (Fin N) (Fin N) ℂ} (hρ : ρ.PosSemidef) : (Φ.apply ρ).PosSemidef

Complete positivity (forward, single copy): the channel preserves positive semidefiniteness. Each Kraus term Kₖ ρ Kₖ† is PSD when ρ is (mul_mul_conjTranspose_same), and PSD is closed under sums.

theorem CSD.LF2.QuantumChannel.apply_trace {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (ρ : Matrix (Fin N) (Fin N) ℂ) : (Φ.apply ρ).trace = ρ.trace

Trace preservation: Tr(Φ(ρ)) = Tr(ρ). Trace cyclicity turns each Tr(Kₖ ρ Kₖ†) into Tr(Kₖ† Kₖ ρ), and the constraint ∑ₖ Kₖ† Kₖ = 1 collapses the sum to Tr(ρ).

noncomputable def CSD.LF2.QuantumChannel.channelApply {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (ρ : DensityOperator N) : DensityOperator M

CPTP-forward: a channel maps density operators to density operators. Φ(ρ) is Hermitian, PSD, and trace one — a genuine density operator on the output system. This is the operational content that quantum channels are the right notion of general (open-system) dynamics.

Equations

• Φ.channelApply ρ = { M := Φ.apply ρ.M, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.LF2.QuantumChannel.channelApply_M {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (ρ : DensityOperator N) : (Φ.channelApply ρ).M = Φ.apply ρ.M

noncomputable def CSD.LF2.QuantumChannel.unitaryChannel {N : ℕ} (U : Matrix (Fin N) (Fin N) ℂ) (hU : U.conjTranspose * U = 1) : QuantumChannel (Fin 1) N N

Unitary conjugation is a channel ρ ↦ U ρ U† (closed, reversible dynamics as the single-Kraus special case).

Equations

• CSD.LF2.QuantumChannel.unitaryChannel U hU = { kraus := fun (x : Fin 1) => U, isTracePreserving := ⋯ }

@[simp]

theorem CSD.LF2.QuantumChannel.unitaryChannel_apply {N : ℕ} (U : Matrix (Fin N) (Fin N) ℂ) (hU : U.conjTranspose * U = 1) (ρ : Matrix (Fin N) (Fin N) ℂ) : (unitaryChannel U hU).apply ρ = U * ρ * U.conjTranspose

noncomputable def CSD.LF2.QuantumChannel.comp {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {N M P : ℕ} (Ψ : QuantumChannel κ M P) (Φ : QuantumChannel ι N M) : QuantumChannel (κ × ι) N P

Channels compose: the composite Ψ ∘ Φ has Kraus family {Ψₐ Φₖ}. The constraint follows by inserting ∑ₐ Ψₐ† Ψₐ = 1 into ∑ₖ Φₖ† (∑ₐ Ψₐ† Ψₐ) Φₖ = ∑ₖ Φₖ† Φₖ = 1.

Equations

• Ψ.comp Φ = { kraus := fun (p : κ × ι) => Ψ.kraus p.1 * Φ.kraus p.2, isTracePreserving := ⋯ }

theorem CSD.LF2.QuantumChannel.cptp_capstone {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (ρ : DensityOperator N) : (Φ.apply ρ.M).PosSemidef ∧ (Φ.apply ρ.M).trace = 1

CPTP-forward capstone (tranche 1). A quantum channel (Kraus form) sends density operators to density operators; unitary conjugation is a channel; channels compose. So CPTP maps are a genuine composition monoid of state transformations extending unitary evolution.

Tranche 2 — Stinespring dilation

Every channel is "a unitary/isometric embedding into a larger system + environment, then trace out the environment". The Kraus operators stack into an isometry V : Fin N → Fin M × ι, and the channel is Φ(ρ) = Tr_E(V ρ V†).

noncomputable def CSD.LF2.QuantumChannel.dilation {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : Matrix (Fin M × ι) (Fin N) ℂ

The Stinespring dilation isometry. The Kraus family stacked into one operator V : Fin N → Fin M × ι, V(m,k) n = Kₖ m n (the environment ι records which Kraus branch).

Equations

• Φ.dilation a n = Φ.kraus a.2 a.1 n

@[simp]

theorem CSD.LF2.QuantumChannel.dilation_apply {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (a : Fin M × ι) (n : Fin N) : Φ.dilation a n = Φ.kraus a.2 a.1 n

theorem CSD.LF2.QuantumChannel.dilation_isometry {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : Φ.dilation.conjTranspose * Φ.dilation = 1

The dilation is an isometry: V† V = 1. Exactly the trace-preservation constraint ∑ₖ Kₖ† Kₖ = 1 reindexed over the stacked output Fin M × ι.

theorem CSD.LF2.QuantumChannel.stinespring {ι : Type u_1} [Fintype ι] {N M : ℕ} [DecidableEq ι] (Φ : QuantumChannel ι N M) (ρ : Matrix (Fin N) (Fin N) ℂ) : QuantumInfo.partialTraceRight (Φ.dilation * ρ * Φ.dilation.conjTranspose) = Φ.apply ρ

Stinespring dilation: Φ(ρ) = Tr_E(V ρ V†). The channel is unitary/isometric evolution into system ⊗ environment followed by tracing out the environment — the structural statement that open-system dynamics is closed dynamics on a larger space.

Tranche 3 — the Choi matrix (complete-positivity witness)

The Choi matrix C_Φ = ∑ₖ vec(Kₖ) vec(Kₖ)† is positive semidefinite — the Choi–Jamiołkowski witness of complete positivity (the "easy" direction of Choi's theorem: a Kraus-form channel has PSD Choi matrix).

noncomputable def CSD.LF2.QuantumChannel.choiMatrix {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : Matrix (Fin M × Fin N) (Fin M × Fin N) ℂ

The Choi matrix C_Φ ∈ Matrix (Fin M × Fin N), C_Φ (m,n)(m',n') = ∑ₖ Kₖ(m,n) · conj(Kₖ(m',n')) — the sum of the rank-one outer products of the vectorised Kraus operators.

Equations

• Φ.choiMatrix = ∑ 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.QuantumChannel.choiMatrix_apply {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (p q : Fin M × Fin N) : Φ.choiMatrix p q = ∑ k : ι, Φ.kraus k p.1 p.2 * star (Φ.kraus k q.1 q.2)

theorem CSD.LF2.QuantumChannel.choiMatrix_posSemidef {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : Φ.choiMatrix.PosSemidef

Complete positivity: the Choi matrix is positive semidefinite. Each term vec(Kₖ) vec(Kₖ)† is a rank-one PSD outer product, and PSD is closed under sums. This is the Choi–Jamiołkowski witness that a Kraus-form channel is completely positive.