LF6-2 (bounded core): the qubit T2 dephasing quantum dynamical semigroup

Category: 6-Local (the continuous-time open-system de-isolation frontier, the "living-history" tier).

LF6-D realises measurement as a single deterministic de-isolation flow step. LF6-2 asks for the continuous-time open-system version: a one-parameter quantum dynamical semigroup (the solution of a Lindblad master equation) implementing decoherence. This module builds the canonical bounded instance — the qubit T2 dephasing semigroup — as a self-contained computation:

Φ_t(ρ) = [[ρ₀₀,           e^{-γt}·ρ₀₁],
          [e^{-γt}·ρ₁₀,   ρ₁₁      ]].

This is the exact solution of the Lindblad dephasing equation dρ/dt = γ(σ_z ρ σ_z − ρ)/2 (dephasing rate γ = 1/T2). We prove the defining semigroup and open-system properties, axiom-free:

• dephasingChannel_zero — Φ_0 = id (the semigroup identity);
• dephasingChannel_semigroup — Φ_s ∘ Φ_t = Φ_{s+t} (the Markovian composition law);
• dephasingChannel_trace — tr Φ_t(ρ) = tr ρ (trace preservation — it is a channel);
• dephasingChannel_populations — the diagonal ρ₀₀, ρ₁₁ (the pointer populations) are conserved: dephasing is population-preserving (pure T2, no T1 relaxation);
• dephasingChannel_coherence — the off-diagonal coherence decays exactly as e^{-γt}·ρ₀₁;
• dephasingChannel_coherence_tendsto_zero — for γ > 0 the coherence → 0 as t → ∞, so the state is driven to its pointer-diagonal (decohered) form: continuous-time einselection.

Honest scope

This is the T2 dephasing instance — a genuine continuous-time de-isolation semigroup with monotone decoherence to the pointer basis (coherence → 0, populations preserved). It is the bounded core of LF6-2. Deferred (the general residual): the general Lindblad generator (dρ/dt = -i[H,ρ] + Σ L_k ρ L_k† − ½{L_k†L_k, ρ}), its complete positivity, and the T1 amplitude-damping channel — the full open-system tier. The generator/ODE derivation (that Φ_t = e^{tℒ} for the Lindblad ℒ) is not built here; the semigroup is exhibited directly as the physical content. Reuses only Mathlib matrix + Real.exp facts (CSD-free).

Reference: specs/future-work.md (LF6-2).

noncomputable def CSD.LF6.dephasingChannel (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin 2) (Fin 2) ℂ

The qubit T2 dephasing channel at time t with rate γ: the diagonal (population) entries are untouched, the off-diagonal (coherence) entries are damped by e^{-γt}. The exact solution of the Lindblad dephasing equation.

Equations

• CSD.LF6.dephasingChannel γ t ρ = !![ρ 0 0, ↑(Real.exp (-(γ * t))) * ρ 0 1; ↑(Real.exp (-(γ * t))) * ρ 1 0, ρ 1 1]

@[simp]

theorem CSD.LF6.dephasingChannel_apply_00 (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ t ρ 0 0 = ρ 0 0

@[simp]

theorem CSD.LF6.dephasingChannel_apply_11 (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ t ρ 1 1 = ρ 1 1

@[simp]

theorem CSD.LF6.dephasingChannel_apply_01 (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ t ρ 0 1 = ↑(Real.exp (-(γ * t))) * ρ 0 1

@[simp]

theorem CSD.LF6.dephasingChannel_apply_10 (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ t ρ 1 0 = ↑(Real.exp (-(γ * t))) * ρ 1 0

theorem CSD.LF6.dephasingChannel_zero (γ : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ 0 ρ = ρ

Semigroup identity Φ_0 = id. At t = 0 the dephasing channel is the identity (e^0 = 1).

theorem CSD.LF6.dephasingChannel_semigroup (γ s t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ s (dephasingChannel γ t ρ) = dephasingChannel γ (s + t) ρ

The Markovian semigroup law Φ_s ∘ Φ_t = Φ_{s+t}. The dephasing channels compose as a one-parameter semigroup: e^{-γs}·e^{-γt} = e^{-γ(s+t)}. This is the defining property of a quantum dynamical (Markovian) semigroup — memoryless continuous-time evolution.

theorem CSD.LF6.dephasingChannel_trace (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : (dephasingChannel γ t ρ).trace = ρ.trace

Trace preservation. tr Φ_t(ρ) = tr ρ: dephasing preserves the trace (probability), so it is a genuine trace-preserving channel.

theorem CSD.LF6.dephasingChannel_populations (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ t ρ 0 0 = ρ 0 0 ∧ dephasingChannel γ t ρ 1 1 = ρ 1 1

Population preservation (pure T2, no T1). The diagonal entries — the pointer-basis populations — are conserved for all t: dephasing removes coherence without relaxing populations.

theorem CSD.LF6.dephasingChannel_coherence (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingChannel γ t ρ 0 1 = ↑(Real.exp (-(γ * t))) * ρ 0 1

Coherence decay (the decoherence law). The off-diagonal coherence decays exactly as Φ_t(ρ)₀₁ = e^{-γt}·ρ₀₁ — exponential suppression at rate γ = 1/T2.

theorem CSD.LF6.dephasing_decay {γ : ℝ} (hγ : 0 < γ) : Filter.Tendsto (fun (t : ℝ) => ↑(Real.exp (-(γ * t)))) Filter.atTop (nhds 0)

The complex-valued decay factor e^{-γt} → 0 as t → ∞ (for γ > 0).

theorem CSD.LF6.dephasingChannel_coherence_tendsto_zero {γ : ℝ} (hγ : 0 < γ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : Filter.Tendsto (fun (t : ℝ) => dephasingChannel γ t ρ 0 1) Filter.atTop (nhds 0)

Monotone decoherence: the coherence vanishes as t → ∞ (for γ > 0). The off-diagonal element Φ_t(ρ)₀₁ → 0: continuous-time de-isolation drives the state to the pointer (diagonal) basis — its populations survive (dephasingChannel_populations), its coherence dies. This is the continuous-time realisation of einselection to the pointer basis.