Stinespring dilation of a Kraus-form quantum channel

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

This file (phase C2 of specs/channels-plan.md) gives the Stinespring / dilation form of a finite-dimensional quantum channel and the Kraus ↔ Stinespring bridge. A channel Φ : Matrix n n ℂ → Matrix m m ℂ is realised as

Φ(ρ) = traceRight (V * ρ * Vᴴ), V : Matrix (m × e) n ℂ, Vᴴ V = 1,

i.e. an isometric embedding V into system ⊗ environment followed by tracing out the environment e. Operationally: dilate to a closed (isometric) evolution on the enlarged state space, then average over the environment.

The whole bridge rests on a single block-algebra identity. For any V : Matrix (m × e) n ℂ, its environment blocks krausBlock V i := (a, j) ↦ V (a, i) j satisfy

• sum_krausBlock_conjTranspose_mul: ∑ᵢ (krausBlock V i)ᴴ * (krausBlock V i) = Vᴴ * V — so V is an isometry iff the blocks are trace-preserving Kraus operators;
• traceRight_conj_eq_sum_krausBlock: traceRight (V * ρ * Vᴴ) = ∑ᵢ (krausBlock V i) ρ (krausBlock V i)ᴴ — so the environment-averaged joint conjugation is exactly the Kraus action.

From these:

• Channel.ofIsometry V hV — the channel whose Kraus operators are the env-blocks of an isometry V (kraus_of_isometry direction), with ofIsometry_apply identifying its action with traceRight (V ρ Vᴴ);
• Channel.stinespringIsom Φ — the stacked-Kraus isometry of a channel (dilation_exists direction), stinespringIsom_isom : (stinespringIsom Φ)ᴴ (stinespringIsom Φ) = 1, and apply_eq_traceRight_stinespring : Φ.apply ρ = traceRight (stinespringIsom Φ * ρ * (stinespringIsom Φ)ᴴ).

CSD reading (see specs/channels-plan.md §3). The Stinespring isometry is a measure-preserving joint flow on Σ_sys × Σ_env and traceRight is the environment average, so a channel is the environment-marginal of a genuine Φ ≠ id flow — the structural on-ramp to the dynamics frontier (decoherence = environment volume flow).

def QuantumInfo.krausBlock {n : Type u_1} {m : Type u_2} {e : Type u_3} (V : Matrix (m × e) n ℂ) (i : e) : Matrix m n ℂ

The environment block i of a matrix V : Matrix (m × e) n ℂ: the operator ℂⁿ → ℂᵐ selecting the i-th environment slot, (krausBlock V i) a j = V (a, i) j.

Equations

• QuantumInfo.krausBlock V i = Matrix.of fun (a : m) (j : n) => V (a, i) j

@[simp]

theorem QuantumInfo.krausBlock_apply {n : Type u_1} {m : Type u_2} {e : Type u_3} [Fintype n] [Fintype m] [Fintype e] [DecidableEq n] (V : Matrix (m × e) n ℂ) (i : e) (a : m) (j : n) : krausBlock V i a j = V (a, i) j

theorem QuantumInfo.sum_krausBlock_conjTranspose_mul {n : Type u_1} {m : Type u_2} {e : Type u_3} [Fintype n] [Fintype m] [Fintype e] [DecidableEq n] (V : Matrix (m × e) n ℂ) : ∑ i : e, (krausBlock V i).conjTranspose * krausBlock V i = V.conjTranspose * V

The defining block identity: ∑ᵢ (krausBlock V i)ᴴ (krausBlock V i) = Vᴴ V. So V is an isometry exactly when its environment blocks are trace-preserving Kraus operators.

theorem QuantumInfo.traceRight_conj_eq_sum_krausBlock {n : Type u_1} {m : Type u_2} {e : Type u_3} [Fintype n] [Fintype m] [Fintype e] [DecidableEq n] (V : Matrix (m × e) n ℂ) (ρ : Matrix n n ℂ) : (V * ρ * V.conjTranspose).traceRight = ∑ i : e, krausBlock V i * ρ * (krausBlock V i).conjTranspose

The action identity: the environment-averaged joint conjugation of V is the Kraus action of its environment blocks, traceRight (V ρ Vᴴ) = ∑ᵢ (krausBlock V i) ρ (krausBlock V i)ᴴ.

noncomputable def QuantumInfo.Channel.ofIsometry {n : Type u_1} {m : Type u_2} {e : Type u_3} [Fintype n] [Fintype m] [Fintype e] [DecidableEq n] (V : Matrix (m × e) n ℂ) (hV : V.conjTranspose * V = 1) : Channel n m e

Kraus ⇐ isometry (kraus_of_isometry). The channel whose Kraus operators are the environment blocks of an isometry V : Matrix (m × e) n ℂ (Vᴴ V = 1). Its action is the Stinespring form ρ ↦ traceRight (V ρ Vᴴ) (see ofIsometry_apply).

Equations

• QuantumInfo.Channel.ofIsometry V hV = { kraus := QuantumInfo.krausBlock V, tp := ⋯ }

theorem QuantumInfo.Channel.ofIsometry_apply {n : Type u_1} {m : Type u_2} {e : Type u_3} [Fintype n] [Fintype m] [Fintype e] [DecidableEq n] (V : Matrix (m × e) n ℂ) (hV : V.conjTranspose * V = 1) (ρ : Matrix n n ℂ) : (ofIsometry V hV).apply ρ = (V * ρ * V.conjTranspose).traceRight

The action of ofIsometry V hV is the Stinespring form: dilate by V, then trace out the environment.

def QuantumInfo.Channel.stinespringIsom {n : Type u_1} {m : Type u_2} {ι : Type u_4} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) : Matrix (m × ι) n ℂ

Isometry ⇐ Kraus (dilation_exists). The Stinespring isometry of a channel, stacking its Kraus operators along the environment index ι: (stinespringIsom Φ) (a, i) j = (Φ.kraus i) a j.

Equations

• Φ.stinespringIsom = Matrix.of fun (p : m × ι) (j : n) => Φ.kraus p.2 p.1 j

@[simp]

theorem QuantumInfo.Channel.krausBlock_stinespringIsom {n : Type u_1} {m : Type u_2} {ι : Type u_4} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (i : ι) : krausBlock Φ.stinespringIsom i = Φ.kraus i

theorem QuantumInfo.Channel.stinespringIsom_isom {n : Type u_1} {m : Type u_2} {ι : Type u_4} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) : Φ.stinespringIsom.conjTranspose * Φ.stinespringIsom = 1

The Stinespring dilation stinespringIsom Φ is a genuine isometry: (stinespringIsom Φ)ᴴ (stinespringIsom Φ) = 1, exactly the trace-preserving constraint.

theorem QuantumInfo.Channel.apply_eq_traceRight_stinespring {n : Type u_1} {m : Type u_2} {ι : Type u_4} [Fintype n] [Fintype m] [Fintype ι] [DecidableEq n] (Φ : Channel n m ι) (ρ : Matrix n n ℂ) : Φ.apply ρ = (Φ.stinespringIsom * ρ * Φ.stinespringIsom.conjTranspose).traceRight

Stinespring = Kraus. The channel action is the dilate-then-trace form for the stacked-Kraus isometry: Φ(ρ) = traceRight (V ρ Vᴴ) with V = stinespringIsom Φ.