LF6-9: the general Lindblad (GKSL) generator and its CPTP-generating structure

Category: 6-Local (the continuous-time open-system de-isolation frontier — the generator tier).

LF6/DephasingSemigroup.lean and LF6/AmplitudeDamping.lean exhibit the two canonical qubit dissipators (T2 dephasing, T1 amplitude damping) directly, as the exact solutions of their master equations — but neither defines the underlying generator, proves complete positivity, or links the exhibited channel to a generator. This module supplies the missing generator tier: the general Lindblad / GKSL generator and the structural properties that make its flow a CPTP semigroup.

ℒ(ρ) = −i[H, ρ] + Σₖ ( Lₖ ρ Lₖ† − ½{Lₖ†Lₖ, ρ} )          (`lindbladGenerator`)

Main results

• lindbladGenerator / lindbladDissipator — the GKSL generator and one dissipator term, for any Hamiltonian H and jump operators Lₖ on Matrix n n ℂ.
• lindbladGenerator_trace — trace annihilation tr ℒ(ρ) = 0: the commutator and every dissipator are traceless (cyclicity + the ½{L†L,ρ} counterterm), so the generated flow is trace-preserving.
• lindbladGenerator_isHermitian — ℒ maps Hermitian to Hermitian (for H Hermitian): the flow preserves Hermiticity, so density operators stay Hermitian.
• lindblad_dissipation_posSemidef — the dissipative jump part Σₖ Lₖ ρ Lₖ† preserves positive semidefiniteness — the same Choi–Kraus CP witness (PosSemidef.mul_mul_conjTranspose_same, posSemidef_sum) used for QuantumChannel.apply. This is the complete-positivity structure of the dissipator.

The dephasing instance (generator ↔ exhibited semigroup)

• dephasingGenerator + dephasingGenerator_eq_lindblad — the T2 generator (γ/2)(σ_z ρ σ_z − ρ) is the GKSL generator with H = 0 and the single jump operator L = √(γ/2)·σ_z (so dephasing is a Lindblad instance).
• dephasingChannel_master_equation — the exhibited dephasingChannel solves its master equation: d/dt Φ_t(ρ) = ℒ_deph(Φ_t(ρ)) entrywise. This is the concrete Φ_t = e^{tℒ} content — the exhibited semigroup is genuinely the generator's flow, not merely asserted to be.

Honest scope

The generator, its trace/Hermiticity/CP structure, and the dephasing generator↔flow correspondence are proved here. Deferred (the genuinely Mathlib-scale residual): complete positivity of the exponentiated map e^{tℒ} for an arbitrary GKSL generator (as opposed to the concrete qubit channels, whose CP is their exhibited Kraus form) — that needs matrix-exponential positivity in the L2-operator norm scope. The generator-level CP witness (lindblad_dissipation_posSemidef) is the buildable core.

References: LF2/QuantumChannel.lean (apply_posSemidef, the Kraus CP witness reused here); LF2/ChoiConverse.lean (choi_iff_posSemidef, the CP↔PSD-Choi characterisation); LF6/DephasingSemigroup.lean (dephasingChannel, the exhibited T2 semigroup); specs/future-work.md (LF6-2, LF6-9); specs/BACKLOG.md.

noncomputable def CSD.LF6.lindbladDissipator {n : Type u_1} [Fintype n] (L ρ : Matrix n n ℂ) : Matrix n n ℂ

One Lindblad dissipator term D_L(ρ) = L ρ L† − ½(L†L ρ + ρ L†L) (the k-th GKSL summand).

Equations

• CSD.LF6.lindbladDissipator L ρ = L * ρ * L.conjTranspose - (1 / 2) • (L.conjTranspose * L * ρ + ρ * (L.conjTranspose * L))

noncomputable def CSD.LF6.lindbladGenerator {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (ρ : Matrix n n ℂ) : Matrix n n ℂ

The general Lindblad (GKSL) generator ℒ(ρ) = −i[H,ρ] + Σₖ D_{Lₖ}(ρ) for a Hamiltonian H and jump operators L : ι → Matrix n n ℂ.

Equations

• CSD.LF6.lindbladGenerator H L ρ = -Complex.I • (H * ρ - ρ * H) + ∑ k : ι, CSD.LF6.lindbladDissipator (L k) ρ

Trace annihilation ⟹ the flow is trace-preserving

theorem CSD.LF6.lindbladDissipator_trace {n : Type u_1} [Fintype n] (L ρ : Matrix n n ℂ) : (lindbladDissipator L ρ).trace = 0

A single dissipator is traceless. tr(L ρ L†) = tr(L†L ρ) (cyclicity) exactly cancels the ½{L†L, ρ} counterterm.

theorem CSD.LF6.lindbladGenerator_trace {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (ρ : Matrix n n ℂ) : (lindbladGenerator H L ρ).trace = 0

Trace annihilation tr ℒ(ρ) = 0. The commutator is traceless (tr(Hρ) = tr(ρH)) and every dissipator is traceless, so the Lindblad flow preserves the trace — it is trace-preserving.

Complete positivity of the dissipative jump part

theorem CSD.LF6.lindblad_dissipation_posSemidef {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] (L : ι → Matrix n n ℂ) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : (∑ k : ι, L k * ρ * (L k).conjTranspose).PosSemidef

The dissipative jump part Σₖ Lₖ ρ Lₖ† preserves positive semidefiniteness. Each Lₖ ρ Lₖ† is PSD when ρ is (PosSemidef.mul_mul_conjTranspose_same) and PSD is closed under sums — the same Choi–Kraus complete-positivity witness as QuantumChannel.apply_posSemidef.

Hermiticity preservation ⟹ the flow keeps states Hermitian

theorem CSD.LF6.isHermitian_mul_mul_conjTranspose {n : Type u_1} [Fintype n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (L : Matrix n n ℂ) : (L * ρ * L.conjTranspose).IsHermitian

L ρ L† is Hermitian when ρ is.

theorem CSD.LF6.lindbladDissipator_isHermitian {n : Type u_1} [Fintype n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (L : Matrix n n ℂ) : (lindbladDissipator L ρ).IsHermitian

A single dissipator preserves Hermiticity. LρL† is Hermitian, as is ½{L†L, ρ} (the anticommutator of the Hermitian L†L with the Hermitian ρ); their difference is Hermitian.

theorem CSD.LF6.lindbladGenerator_isHermitian {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] {H : Matrix n n ℂ} (hH : H.IsHermitian) {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (L : ι → Matrix n n ℂ) : (lindbladGenerator H L ρ).IsHermitian

The Lindblad generator preserves Hermiticity (for H Hermitian): ℒ(ρ) is Hermitian whenever ρ is, so a Hermitian density operator stays Hermitian under the flow. The commutator part −i[H,ρ] is Hermitian ((−i[H,ρ])† = i[ρ,H]·… = −i[H,ρ]) and each dissipator is Hermitian.

The T2 dephasing instance: generator ↔ exhibited semigroup

The qubit dephasing generator (γ/2)(σ_z ρ σ_z − ρ) is the GKSL generator with H = 0 and one jump operator L = √(γ/2)·σ_z, and the exhibited dephasingChannel solves its master equation.

noncomputable def CSD.LF6.sigmaZ : Matrix (Fin 2) (Fin 2) ℂ

The Pauli σ_z = diag(1, −1).

Equations

• CSD.LF6.sigmaZ = !![1, 0; 0, -1]

@[simp]

theorem CSD.LF6.sigmaZ_mul_self : sigmaZ * sigmaZ = 1

@[simp]

theorem CSD.LF6.sigmaZ_conjTranspose : sigmaZ.conjTranspose = sigmaZ

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

The T2 dephasing generator ℒ_deph(ρ) = (γ/2)(σ_z ρ σ_z − ρ) — the RHS of the dephasing master equation dρ/dt = ℒ_deph(ρ).

Equations

• CSD.LF6.dephasingGenerator γ ρ = (↑γ / 2) • (CSD.LF6.sigmaZ * ρ * CSD.LF6.sigmaZ - ρ)

@[simp]

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

@[simp]

theorem CSD.LF6.dephasingGenerator_apply_11 (γ : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingGenerator γ ρ 1 1 = 0

@[simp]

theorem CSD.LF6.dephasingGenerator_apply_01 (γ : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingGenerator γ ρ 0 1 = -↑γ * ρ 0 1

@[simp]

theorem CSD.LF6.dephasingGenerator_apply_10 (γ : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingGenerator γ ρ 1 0 = -↑γ * ρ 1 0

theorem CSD.LF6.dephasingGenerator_eq_lindblad {γ : ℝ} (hγ : 0 ≤ γ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : dephasingGenerator γ ρ = lindbladGenerator 0 (fun (x : Fin 1) => ↑√(γ / 2) • sigmaZ) ρ

Dephasing is a Lindblad instance. For γ ≥ 0, the T2 dephasing generator is the GKSL generator with no Hamiltonian and the single jump operator L = √(γ/2)·σ_z: (γ/2)(σ_z ρ σ_z − ρ) = ℒ(ρ) with H = 0, L₀ = √(γ/2)·σ_z. So the general trace/Hermiticity/CP structure specialises to dephasing.

The dephasing master equation: the exhibited semigroup is the generator's flow

theorem CSD.LF6.hasDerivAt_expDecay (γ t : ℝ) (c : ℂ) : HasDerivAt (fun (τ : ℝ) => ↑(Real.exp (-(γ * τ))) * c) (-↑γ * ↑(Real.exp (-(γ * t))) * c) t

The complex decay factor e^{-γt}·c has derivative −γ·e^{-γt}·c in t.

theorem CSD.LF6.dephasingChannel_master_equation (γ : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) (t : ℝ) (i j : Fin 2) : HasDerivAt (fun (τ : ℝ) => dephasingChannel γ τ ρ i j) (dephasingGenerator γ (dephasingChannel γ t ρ) i j) t

The dephasing master equation. The exhibited T2 semigroup dephasingChannel solves its Lindblad master equation entrywise: d/dt Φ_t(ρ) = ℒ_deph(Φ_t(ρ)). The populations are stationary (ℒ_deph kills the diagonal, Φ is constant there); each coherence decays at rate γ (d/dt(e^{-γt}ρ₀₁) = −γ·e^{-γt}ρ₀₁), which is exactly ℒ_deph(Φ_t(ρ)) off-diagonal. So the directly exhibited channel genuinely is the generator's flow (Φ_t = e^{tℒ}), not merely asserted to be.