The bridge between LF2.QuantumChannel and QuantumInfo.Channel

Category: 3-Local (W5 of specs/qit-chain-scoping.md, second half).

The corpus carries two Kraus-form channel types: CSD.LF2.QuantumChannel ι N M (Fin-indexed, 2026-05, with the Stinespring dilation, the Choi matrix and Choi's theorem built on it) and QuantumInfo.Channel n m ι (index-generic, the type every entropy, distance and data-processing theorem of Mathlib/QuantumInfo/ takes). They are the same data with the index order swapped, and until 2026-09-11 nothing said so, so no QIT theorem applied to an LF2 channel. This module is the bridge:

• toChannel / ofChannel / channelEquiv — the equivalence, with toChannel_apply, ofChannel_apply (the actions agree, by rfl) and channelApply_M_eq for density operators;
• toChannel_stinespringIsom (the LF2 dilation is the QuantumInfo Stinespring isometry), unitaryChannel_apply_eq, toChannel_comp — the derived notions correspond;
• ★ traceDist_channelApply_le — the data-processing inequality for LF2 channels, one exact through the bridge.

Interface status. CSD.LF2.QuantumChannel is henceforth an interface to QuantumInfo.Channel: kept for its Choi results (choiMatrix, choi_iff_posSemidef in LF2/ChoiConverse.lean) and its existing consumers, not extended. New work states channels as QuantumInfo.Channel and moves through toChannel / ofChannel when it needs the Choi layer.

References: specs/qit-chain-scoping.md (W5); LF2/QuantumChannel.lean; Mathlib/QuantumInfo/{Channel,Stinespring,CanonicalChannels,DataProcessing,ChannelComp}.lean; LF6/DecoherenceChannel.lean (W5's witness half).

The bridge LF2.QuantumChannel ↔ QuantumInfo.Channel

def CSD.LF2.QuantumChannel.toChannel {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : QuantumInfo.Channel (Fin N) (Fin M) ι

The LF2 channel as a QuantumInfo.Channel: the same Kraus family, index order swapped.

Equations

• Φ.toChannel = { kraus := Φ.kraus, tp := ⋯ }

def CSD.LF2.QuantumChannel.ofChannel {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumInfo.Channel (Fin N) (Fin M) ι) : QuantumChannel ι N M

A QuantumInfo.Channel between Fin-indexed spaces as an LF2 channel.

Equations

• CSD.LF2.QuantumChannel.ofChannel Φ = { kraus := Φ.kraus, isTracePreserving := ⋯ }

@[simp]

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

@[simp]

theorem CSD.LF2.QuantumChannel.ofChannel_kraus {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumInfo.Channel (Fin N) (Fin M) ι) : (ofChannel Φ).kraus = Φ.kraus

def CSD.LF2.QuantumChannel.channelEquiv {ι : Type u_1} [Fintype ι] {N M : ℕ} : QuantumChannel ι N M ≃ QuantumInfo.Channel (Fin N) (Fin M) ι

The two channel types are the same data.

Equations

• CSD.LF2.QuantumChannel.channelEquiv = { toFun := CSD.LF2.QuantumChannel.toChannel, invFun := CSD.LF2.QuantumChannel.ofChannel, left_inv := ⋯, right_inv := ⋯ }

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

The actions agree.

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

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

The action on density operators is the QuantumInfo action on the underlying matrix.

theorem CSD.LF2.QuantumChannel.toChannel_stinespringIsom {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) : Φ.toChannel.stinespringIsom = Φ.dilation

The LF2 dilation is the QuantumInfo Stinespring isometry.

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

The LF2 unitary channel and the QuantumInfo one act identically.

theorem CSD.LF2.QuantumChannel.toChannel_comp {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {N M P : ℕ} (Ψ : QuantumChannel κ M P) (Φ : QuantumChannel ι N M) : (Ψ.comp Φ).toChannel = Ψ.toChannel.comp Φ.toChannel

Composition is respected.

theorem CSD.LF2.QuantumChannel.traceDist_channelApply_le {ι : Type u_1} [Fintype ι] {N M : ℕ} (Φ : QuantumChannel ι N M) (ρ σ : DensityOperator N) : QuantumInfo.traceDist ⋯ ≤ QuantumInfo.traceDist ⋯

★ The QIT layer applies to LF2 channels through the bridge: the data-processing inequality for the trace distance of two density operators under an LF2 channel.