The de-isolation channel: decohereReduced is the action of a QuantumInfo.Channel

Category: 3-Local (W5's witness half, specs/qit-chain-scoping.md; the LF6 instance of LF2/FlowChannel.lean).

LF6/Decoherence.lean computes the system's reduced state after the von Neumann de-isolation and the pointer trace, decohereReduced ψ = Tr_ptr (V |ψ⟩⟨ψ| Vᴴ) with V = vnDilationV N = vnUnitary N * embedGround N. Until now it was a matrix nothing in Mathlib/QuantumInfo/ could consume as a channel output. This module states it as one:

• embedGround_eq_embedEnv — LF5's ground embedding is embedEnv with the ready vector a₀ = e₀, so vnDilationV N is the isometry U · embedEnv e₀ of stinespringChannel;
• deisolationChannel N — the de-isolation channel, the Stinespring channel of vnUnitary N with the apparatus ready in a₀: a QuantumInfo.Channel (Fin N) (Fin N) (Fin N);
• ★ deisolationChannel_apply_outerProduct — (deisolationChannel N).apply |ψ⟩⟨ψ| = decohereReduced ψ, and deisolationChannel_apply on any input.

So every channel theorem of the QIT layer (apply_posSemidef, apply_trace, data processing, Stinespring.lean) applies to the decohered state by instantiation, and the LF6 decoherence results become statements about a channel produced by a Σ-flow (traceRight_barycenter_flow in LF2/FlowChannel.lean with U := vnUnitary N, e₀ := a₀).

Scope: the channel-level bridge for the decohered state. The other half of W5, the equivalence LF2.QuantumChannel ≃ QuantumInfo.Channel with the parallel type marked an interface, is LF2/ChannelBridge.lean.

References: specs/qit-chain-scoping.md (W5, W6); LF2/FlowChannel.lean; LF5/DilationFromFlow.lean (embedGround, vnDilationV, vnDilationV_isom); LF6/Decoherence.lean (decohereReduced, decoherence_dephases).

theorem CSD.LF6.embedGround_eq_embedEnv {N : ℕ} [NeZero N] : LF5.embedGround N = LF2.embedEnv (Fin N) (EuclideanSpace.single 0 1)

The LF5 ground embedding is embedEnv with the ready vector a₀ = e₀.

noncomputable def CSD.LF6.deisolationChannel (N : ℕ) [NeZero N] : QuantumInfo.Channel (Fin N) (Fin N) (Fin N)

The de-isolation channel: the Stinespring channel of the von Neumann coupling with the apparatus ready in a₀.

Equations

• CSD.LF6.deisolationChannel N = CSD.LF2.stinespringChannel (CSD.LF5.vnUnitary N) ⋯ (EuclideanSpace.single 0 1) ⋯

theorem CSD.LF6.deisolationChannel_apply_outerProduct {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) : (deisolationChannel N).apply (LF2.outerProduct ψ) = decohereReduced ψ

★ decohereReduced IS the action of a QuantumInfo.Channel — the de-isolation channel applied to the pure input |ψ⟩⟨ψ|. W5's witness half.

theorem CSD.LF6.deisolationChannel_apply {N : ℕ} [NeZero N] (ρ : Matrix (Fin N) (Fin N) ℂ) : (deisolationChannel N).apply ρ = QuantumInfo.partialTraceRight (LF5.vnDilationV N * ρ * (LF5.vnDilationV N).conjTranspose)

The de-isolation channel on any input is Tr_ptr (V ρ Vᴴ) with V = vnDilationV N.