Finite-dimensional quantum channels (Kraus form)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

A quantum channel Φ : Matrix n n ℂ → Matrix m m ℂ in Kraus form: a finite family of Kraus operators Kᵢ : Matrix m n ℂ with the trace-preserving constraint ∑ᵢ Kᵢᴴ Kᵢ = 1, acting by Φ(ρ) = ∑ᵢ Kᵢ ρ Kᵢᴴ.

This file (phase C1 of specs/channels-plan.md) establishes the type and the core properties: the action is linear, trace-preserving (apply_trace), positive (apply_posSemidef), and Hermiticity-preserving (apply_isHermitian) — so a channel maps density operators to density operators. Complete positivity — positivity of Φ ⊗ id_b for every idle factor — is formalised downstream: CanonicalChannels.lean builds the local channel Channel.tensorRight (Kraus operators Kᵢ ⊗ I_b) and tensorRight_posSemidef is the named CP witness, immediate from this file's apply_posSemidef. The Stinespring dilation lives in Stinespring.lean (C2) and the canonical channels in CanonicalChannels.lean (C3), both landed 2026-06-05 alongside C1.

The Kraus index ι is an arbitrary Fintype (matching CSD.LF2.POVM's convention).

structure QuantumInfo.Channel (n : Type u_1) (m : Type u_2) (ι : Type u_3) [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] : Type (max (max u_1 u_2) u_3)

A finite-dimensional quantum channel in Kraus form: Kraus operators kraus i with the trace-preserving (TP) constraint ∑ᵢ (kraus i)ᴴ (kraus i) = 1. The action is apply ρ = ∑ᵢ (kraus i) ρ (kraus i)ᴴ.

• kraus : ι → Matrix m n ℂ

  The Kraus operators Kᵢ : ℂⁿ → ℂᵐ.

• tp : ∑ i : ι, (self.kraus i).conjTranspose * self.kraus i = 1

  Trace preservation: ∑ᵢ Kᵢᴴ Kᵢ = 1.

noncomputable def QuantumInfo.Channel.apply {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (ρ : Matrix n n ℂ) : Matrix m m ℂ

The action of a channel on an operator: Φ(ρ) = ∑ᵢ Kᵢ ρ Kᵢᴴ.

Equations

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

@[simp]

theorem QuantumInfo.Channel.apply_def {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (ρ : Matrix n n ℂ) : Φ.apply ρ = ∑ i : ι, Φ.kraus i * ρ * (Φ.kraus i).conjTranspose

theorem QuantumInfo.Channel.apply_add {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (ρ σ : Matrix n n ℂ) : Φ.apply (ρ + σ) = Φ.apply ρ + Φ.apply σ

The channel action is additive.

theorem QuantumInfo.Channel.apply_smul {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (c : ℂ) (ρ : Matrix n n ℂ) : Φ.apply (c • ρ) = c • Φ.apply ρ

The channel action commutes with scalar multiplication.

theorem QuantumInfo.Channel.apply_trace {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (ρ : Matrix n n ℂ) : (Φ.apply ρ).trace = ρ.trace

Trace preservation. Tr(Φ ρ) = Tr ρ — the defining TP property, from ∑ᵢ Kᵢᴴ Kᵢ = 1 and trace cyclicity.

theorem QuantumInfo.Channel.apply_posSemidef {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : (Φ.apply ρ).PosSemidef

Positivity. A channel maps positive-semidefinite operators to positive-semidefinite operators: each Kᵢ ρ Kᵢᴴ is PSD, and PSD is closed under finite sums.

theorem QuantumInfo.Channel.apply_isHermitian {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : (Φ.apply ρ).IsHermitian

A channel preserves Hermiticity.

theorem QuantumInfo.Channel.apply_sub {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (ρ σ : Matrix n n ℂ) : Φ.apply (ρ - σ) = Φ.apply ρ - Φ.apply σ

The channel action is subtractive (linearity in the input).

The channel adjoint (Heisenberg dual)

For Φ(ρ) = ∑ᵢ Kᵢ ρ Kᵢᴴ the adjoint (dual / Heisenberg) map is Φ†(P) = ∑ᵢ Kᵢᴴ P Kᵢ, characterised by the trace duality Tr(P · Φ ρ) = Tr(Φ† P · ρ). The TP constraint ∑ᵢ Kᵢᴴ Kᵢ = 1 makes Φ† unital (Φ† 1 = 1); together with positivity this gives 0 ≤ Φ† P ≤ I whenever 0 ≤ P ≤ I, the load-bearing fact for data processing.

noncomputable def QuantumInfo.Channel.adjoint {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (P : Matrix m m ℂ) : Matrix n n ℂ

The adjoint (Heisenberg dual) of a channel: Φ†(P) = ∑ᵢ Kᵢᴴ P Kᵢ.

Equations

• Φ.adjoint P = ∑ i : ι, (Φ.kraus i).conjTranspose * P * Φ.kraus i

@[simp]

theorem QuantumInfo.Channel.adjoint_def {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (P : Matrix m m ℂ) : Φ.adjoint P = ∑ i : ι, (Φ.kraus i).conjTranspose * P * Φ.kraus i

theorem QuantumInfo.Channel.adjoint_unital {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] [DecidableEq m] (Φ : Channel n m ι) : Φ.adjoint 1 = 1

The adjoint is unital: Φ† 1 = 1, directly from the TP constraint ∑ᵢ Kᵢᴴ Kᵢ = 1.

theorem QuantumInfo.Channel.adjoint_posSemidef {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) {P : Matrix m m ℂ} (hP : P.PosSemidef) : (Φ.adjoint P).PosSemidef

The adjoint preserves positive-semidefiniteness: each Kᵢᴴ P Kᵢ is PSD and PSD is closed under finite sums.

theorem QuantumInfo.Channel.adjoint_sub {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (P Q : Matrix m m ℂ) : Φ.adjoint (P - Q) = Φ.adjoint P - Φ.adjoint Q

The adjoint is subtractive (linearity in P).

theorem QuantumInfo.Channel.adjoint_add {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (P Q : Matrix m m ℂ) : Φ.adjoint (P + Q) = Φ.adjoint P + Φ.adjoint Q

The adjoint is additive (linearity in P).

theorem QuantumInfo.Channel.adjoint_le_one {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] [DecidableEq m] (Φ : Channel n m ι) {P : Matrix m m ℂ} (_hP : P.PosSemidef) (hP' : (1 - P).PosSemidef) : (1 - Φ.adjoint P).PosSemidef

0 ≤ P ≤ I ⟹ 0 ≤ Φ† P ≤ I (the half consumed by data processing): unitality + subtractivity give 1 − Φ† P = Φ† (1 − P), PSD by adjoint_posSemidef.

theorem QuantumInfo.Channel.adjoint_trace_mul {n : Type u_1} {m : Type u_2} {ι : Type u_3} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (P : Matrix m m ℂ) (ρ : Matrix n n ℂ) : (P * Φ.apply ρ).trace = (Φ.adjoint P * ρ).trace

Adjoint (trace) duality: Tr(P · Φ ρ) = Tr(Φ† P · ρ). The defining property of the adjoint, via trace cyclicity rotating Kᵢᴴ to the front of each summand.

def QuantumInfo.Channel.id (n : Type u_4) [Fintype n] [DecidableEq n] : Channel n n PUnit.{u_5 + 1}

The identity channel (a single Kraus operator 1).

Equations

• QuantumInfo.Channel.id n = { kraus := fun (x : PUnit.{?u.1 + 1}) => 1, tp := ⋯ }

@[simp]

theorem QuantumInfo.Channel.id_apply (n : Type u_4) [Fintype n] [DecidableEq n] (ρ : Matrix n n ℂ) : (id n).apply ρ = ρ