The Lindblad semigroup: the exponentiated GKSL tier (§Q Q5, LF6-9)

Category: 4-LF (open-system dynamics). The generator tier (LF6/LindbladGenerator.lean) built ℒ(ρ) = −i[H,ρ] + Σₖ D_{Lₖ}(ρ) and proved trace annihilation, Hermiticity preservation, and complete positivity of the jump part. This module exponentiates: Φₜ = e^{tℒ}, for an arbitrary GKSL generator, with the flow-level laws.

• lindbladSemigroup — Φₜ := exp (t • ℒ) in the Banach algebra of continuous endomorphisms of matrix space (the L2-operator scope supplies the norm and completeness, as everywhere in the corpus's matrix-exp work).
• lindbladSemigroup_zero / ★ lindbladSemigroup_add — Φ₀ = 1 and the semigroup law Φ_{s+t} = Φ_s ∘ Φ_t.
• ★★ lindbladSemigroup_hasDerivAt — the master equation: for every state, d/dt (Φₜ ρ) = ℒ(Φₜ ρ). The dephasing instance solved its master equation by hand (dephasingChannel_master_equation); this is the general-generator statement.
• ★ lindbladSemigroup_trace — trace preservation at the flow level, tr (Φₜ ρ) = tr ρ: the exponential series termwise inherits lindbladGenerator_trace (every power ℒⁿ, n ≥ 1 is traceless on any input), so only the identity term survives.
• ★ lindbladSemigroup_conjTranspose — Hermiticity preservation at the flow level: (Φₜ ρ)ᴴ = Φₜ (ρᴴ) for Hermitian H, via the generator intertwining lindbladGenerator_conjTranspose pushed through the series (HasSum.star). Corollary lindbladSemigroup_isHermitian.

Honest scope

Complete positivity of e^{tℒ} is NOT claimed — that is the remaining genuinely-Mathlib-scale half recorded on the LF6-9 row. Superseded 2026-08-20: positivity of e^{tℒ} for every GKSL generator with Hermitian H, at every t ≥ 0, is now proved in LF6/LindbladPositivity.lean (lindbladSemigroup_posSemidef, via the de-skewed Banach-algebra Trotter formula), together with its stability under every ancilla amplification of the generator (lindbladSemigroup_amplified_posSemidef). The "needs a Lie–Trotter limit theorem Mathlib does not have" wall was stale — the theorem was buildable in-corpus. What this module still delivers is the tier below: the semigroup exists, solves the master equation, and preserves trace and Hermiticity for arbitrary H, {Lₖ}.

Proof-engineering note: several scalar-action facts (0 • ℒ = 0, (s+t) • ℒ, commutation of the scaled generators, powers of t • ℒ) are proved pointwise or by module rather than by the generic smul lemmas — the module system blocks the instance-level defeq those lemmas' typeclass paths need (Complex.mulAux is not exposed). Same family as the project_module_system_defeq trap.

Cross-references: specs/future-work.md (LF6-2, LF6-9), specs/BACKLOG.md §Q (Q5) and the GKSL row; Mathlib/Analysis/Matrix/DuhamelBound.lean (the same L2-operator exp scope), LF4/ManyToOneSchrodingerDerived.lean (the closed-system exp(t • A) derivative idiom this reuses).

The generator as a (continuous) linear endomorphism

noncomputable def CSD.LF6.lindbladDissipatorL {n : Type u_1} [Fintype n] [DecidableEq n] (L : Matrix n n ℂ) : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ

One dissipator term as a linear endomorphism of matrix space.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF6.lindbladDissipatorL_apply {n : Type u_1} [Fintype n] [DecidableEq n] (L ρ : Matrix n n ℂ) : (lindbladDissipatorL L) ρ = lindbladDissipator L ρ

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

The GKSL generator as a linear endomorphism of matrix space.

Equations

• CSD.LF6.lindbladGeneratorL H L = -Complex.I • (LinearMap.mulLeft ℂ H - LinearMap.mulRight ℂ H) + ∑ k : ι, CSD.LF6.lindbladDissipatorL (L k)

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

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

The GKSL generator as a continuous linear endomorphism of matrix space, over ℝ (restrictScalars) — the element the exponential acts on. Working in the ℝ-endomorphism algebra keeps every scalar action, the Commute instance, and the exponential's field on a single canonical instance path (the module system blocks cross-path instance defeq; see the proof-engineering note above).

Equations

• CSD.LF6.lindbladGeneratorCLM H L = ContinuousLinearMap.restrictScalars ℝ (LinearMap.toContinuousLinearMap (CSD.LF6.lindbladGeneratorL H L))

@[simp]

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

The semigroup

noncomputable def CSD.LF6.lindbladSemigroup {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) : Matrix n n ℂ →L[ℝ] Matrix n n ℂ

The Lindblad semigroup Φₜ = exp (t ℒ): the flow of the master equation, as a family of continuous endomorphisms of matrix space.

Equations

• CSD.LF6.lindbladSemigroup H L t = NormedSpace.exp (t • CSD.LF6.lindbladGeneratorCLM H L)

@[simp]

theorem CSD.LF6.lindbladSemigroup_zero {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) : lindbladSemigroup H L 0 = 1

At t = 0 the flow is the identity.

theorem CSD.LF6.lindbladSemigroup_add {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (s t : ℝ) : lindbladSemigroup H L (s + t) = lindbladSemigroup H L s * lindbladSemigroup H L t

★ The semigroup law: Φ_{s+t} = Φ_s ∘ Φ_t.

theorem CSD.LF6.lindbladSemigroup_hasDerivAt {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (ρ : Matrix n n ℂ) (t : ℝ) : HasDerivAt (fun (u : ℝ) => (lindbladSemigroup H L u) ρ) (lindbladGenerator H L ((lindbladSemigroup H L t) ρ)) t

★★ The master equation, arbitrary GKSL generator: for every state ρ, the flow satisfies d/dt (Φₜ ρ) = ℒ(Φₜ ρ). The general-generator form of what the dephasing instance solved by hand.

The series form: what the flow does termwise

theorem CSD.LF6.lindbladSemigroup_apply_hasSum {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) (ρ : Matrix n n ℂ) : HasSum (fun (m : ℕ) => ((↑m.factorial)⁻¹ • (t • lindbladGeneratorCLM H L) ^ m) ρ) ((lindbladSemigroup H L t) ρ)

The flow applied to a state, as the exponential series.

theorem CSD.LF6.lindbladGeneratorCLM_smul_pow_succ_trace {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) (m : ℕ) (ρ : Matrix n n ℂ) : (((t • lindbladGeneratorCLM H L) ^ (m + 1)) ρ).trace = 0

Every positive power of the scaled generator is traceless on any input.

theorem CSD.LF6.lindbladSemigroup_trace {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) (ρ : Matrix n n ℂ) : ((lindbladSemigroup H L t) ρ).trace = ρ.trace

★ Trace preservation at the flow level: tr (Φₜ ρ) = tr ρ for every t and every input — the exponential series termwise inherits the generator's trace annihilation, so only the identity term survives.

Hermiticity at the flow level

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

The generator intertwines the adjoint: (ℒρ)ᴴ = ℒ(ρᴴ) for Hermitian H — on arbitrary (not necessarily Hermitian) inputs. The generator-tier lindbladGenerator_isHermitian is the diagonal of this.

theorem CSD.LF6.lindbladGeneratorCLM_smul_pow_conjTranspose {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {H : Matrix n n ℂ} (hH : H.IsHermitian) (L : ι → Matrix n n ℂ) (t : ℝ) (m : ℕ) (ρ : Matrix n n ℂ) : (((t • lindbladGeneratorCLM H L) ^ m) ρ).conjTranspose = ((t • lindbladGeneratorCLM H L) ^ m) ρ.conjTranspose

Powers of the scaled generator intertwine the adjoint.

theorem CSD.LF6.lindbladSemigroup_conjTranspose {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {H : Matrix n n ℂ} (hH : H.IsHermitian) (L : ι → Matrix n n ℂ) (t : ℝ) (ρ : Matrix n n ℂ) : ((lindbladSemigroup H L t) ρ).conjTranspose = (lindbladSemigroup H L t) ρ.conjTranspose

★ Hermiticity preservation at the flow level: (Φₜ ρ)ᴴ = Φₜ (ρᴴ) for Hermitian H — the generator intertwining pushed through the exponential series.

theorem CSD.LF6.lindbladSemigroup_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {H ρ : Matrix n n ℂ} (hH : H.IsHermitian) (L : ι → Matrix n n ℂ) (t : ℝ) (hρ : ρ.IsHermitian) : ((lindbladSemigroup H L t) ρ).IsHermitian

The flow keeps states Hermitian.