Positivity of the Lindblad semigroup — the exponentiated CP tier (Q16's gate)

Category: 4-LF (open-system dynamics — the half LF6/LindbladSemigroup.lean declared out of reach). That module's scope block deferred positivity of e^{tℒ} as needing "a Lie–Trotter/Euler-approximant limit theorem or resolvent positivity, neither of which Mathlib has". The 2026-08-20 gate re-check found the label stale, and this module closes the gap in-corpus. Scoped first in specs/cp-semigroup-plan.md.

Glossary: https://glossary.constraintsurfacedynamics.com/lindblad-equation/ Plain-language, CSD-role and formal statements of the Lindblad equation and its complete positivity, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The route:

• The drift needs no Trotter at all. For Hermitian H the generator splits as ℒ = drift + jump (lindbladGeneratorCLM_split) with drift ρ = Gρ + ρG†, G = −iH − ½ΣL†L (gkslG). Left- and right-multiplication commute, so e^{t·drift} ρ = e^{tG} ρ e^{tG†} (exp_smul_driftCLM_apply) — conjugation, positive at every t (exp_smul_driftCLM_posSemidef).
• The jump exponential is a positive series. jump ρ = ΣLρL† preserves PSD (the generator-tier Choi–Kraus witness), every series term of e^{t·jump} is PSD for t ≥ 0, and PSD passes to limits (posSemidef_of_tendsto, via the dotProduct_mulVec characterisation) — exp_smul_jumpCLM_posSemidef.
• Assemble by the Banach-algebra Lie–Trotter formula (NormedSpace.trotter_product, the de-skewed staging brick): e^{tℒ} is a limit of products of the two positive flows, products of PSD-preserving maps preserve PSD (step_pow_posSemidef), and the limit is PSD.
• ★★ lindbladSemigroup_posSemidef — the flow of every GKSL generator with Hermitian H is a positive map at every t ≥ 0.
• ★ lindbladSemigroup_amplified_posSemidef — the complete-positivity shape: the amplified generator (1 ⊗ H, 1 ⊗ Lₖ) is itself GKSL, so positivity survives every ancilla amplification of the generator — a literal instantiation.
• ★★ idTensor_lindbladSemigroup + ★★ lindbladSemigroup_completelyPositive — the id ⊗ Φ identification (Q23, 2026-08-20): the amplified generator's flow IS id ⊗ Φₜ (blockwise action, exponential-series transport of the blockwise generator through expCLM_apply_hasSum), so the amplified positivity is complete positivity of Φₜ in so many words. Supersession record: this was the module's declared boundary at the Q16 CP-brick landing (the missing block-structure lemma); Q23 delivered it the same week and the boundary retired — see specs/BACKLOG.md (Q23).

References

specs/cp-semigroup-plan.md (scoping); specs/BACKLOG.md (Q16 gate re-check, triage 2026-08-20); LF6/LindbladSemigroup.lean (the flow); LF6/LindbladGenerator.lean (lindblad_dissipation_posSemidef); Mathlib/Analysis/NormedSpace/TrotterGeneral.lean (trotter_product); specs/future-work.md (LF6-9).

PSD is closed under nonnegative scaling and under limits

theorem CSD.LF6.posSemidef_real_smul {n : Type u_1} [Fintype n] {M : Matrix n n ℂ} (hM : M.PosSemidef) {t : ℝ} (ht : 0 ≤ t) : (t • M).PosSemidef

Nonnegative real scaling preserves positive semidefiniteness (instance-free form).

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

The quadratic form of a matrix at a fixed vector, as a linear functional.

Equations

• CSD.LF6.quadFormL x = { toFun := fun (M : Matrix n n ℂ) => star x ⬝ᵥ M.mulVec x, map_add' := ⋯, map_smul' := ⋯ }

theorem CSD.LF6.posSemidef_of_tendsto {n : Type u_1} [Fintype n] {g : ℕ → Matrix n n ℂ} {S : Matrix n n ℂ} (hg : Filter.Tendsto g Filter.atTop (nhds S)) (h : ∀ (i : ℕ), (g i).PosSemidef) : S.PosSemidef

PSD is closed under limits: the limit of a sequence of positive semidefinite matrices is positive semidefinite. Hermiticity passes to the limit by continuity of star; the quadratic form's real part stays nonnegative by ge_of_tendsto, and its imaginary part stays zero.

Left and right multiplication as continuous endomorphisms

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

Left multiplication as a continuous ℝ-endomorphism of matrix space.

Equations

• CSD.LF6.mulLeftCLM A = ContinuousLinearMap.restrictScalars ℝ (LinearMap.toContinuousLinearMap (LinearMap.mulLeft ℂ A))

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

Right multiplication as a continuous ℝ-endomorphism of matrix space.

Equations

• CSD.LF6.mulRightCLM B = ContinuousLinearMap.restrictScalars ℝ (LinearMap.toContinuousLinearMap (LinearMap.mulRight ℂ B))

@[simp]

theorem CSD.LF6.mulLeftCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] (A ρ : Matrix n n ℂ) : (mulLeftCLM A) ρ = A * ρ

@[simp]

theorem CSD.LF6.mulRightCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] (B ρ : Matrix n n ℂ) : (mulRightCLM B) ρ = ρ * B

theorem CSD.LF6.expCLM_apply_hasSum {n : Type u_1} [Fintype n] [DecidableEq n] (T : Matrix n n ℂ →L[ℝ] Matrix n n ℂ) (ρ : Matrix n n ℂ) : HasSum (fun (m : ℕ) => ((↑m.factorial)⁻¹ • T ^ m) ρ) ((NormedSpace.exp T) ρ)

The exponential of any endomorphism, applied: the series form (the lindbladSemigroup_apply_hasSum idiom, for an arbitrary endomorphism).

theorem CSD.LF6.smul_mulLeftCLM_pow_apply {n : Type u_1} [Fintype n] [DecidableEq n] (t : ℝ) (A : Matrix n n ℂ) (m : ℕ) (ρ : Matrix n n ℂ) : ((t • mulLeftCLM A) ^ m) ρ = (t • A) ^ m * ρ

Powers of a scaled left multiplication, applied.

theorem CSD.LF6.smul_mulRightCLM_pow_apply {n : Type u_1} [Fintype n] [DecidableEq n] (t : ℝ) (B : Matrix n n ℂ) (m : ℕ) (ρ : Matrix n n ℂ) : ((t • mulRightCLM B) ^ m) ρ = ρ * (t • B) ^ m

Powers of a scaled right multiplication, applied.

theorem CSD.LF6.exp_smul_mulLeftCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] (t : ℝ) (A ρ : Matrix n n ℂ) : (NormedSpace.exp (t • mulLeftCLM A)) ρ = NormedSpace.exp (t • A) * ρ

The exponential of a scaled left multiplication is left multiplication by the matrix exponential.

theorem CSD.LF6.exp_smul_mulRightCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] (t : ℝ) (B ρ : Matrix n n ℂ) : (NormedSpace.exp (t • mulRightCLM B)) ρ = ρ * NormedSpace.exp (t • B)

The exponential of a scaled right multiplication is right multiplication by the matrix exponential.

The drift/jump split of the GKSL generator

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

The GKSL drift matrix G = −iH − ½ΣL†L: the non-Hermitian effective Hamiltonian whose conjugation action is the drift half of the generator.

Equations

• CSD.LF6.gkslG H L = -Complex.I • H - (1 / 2) • ∑ k : ι, (L k).conjTranspose * L k

noncomputable def CSD.LF6.driftCLM {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 drift half of the generator: ρ ↦ Gρ + ρG†.

Equations

• CSD.LF6.driftCLM H L = CSD.LF6.mulLeftCLM (CSD.LF6.gkslG H L) + CSD.LF6.mulRightCLM (CSD.LF6.gkslG H L).conjTranspose

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

The jump half of the generator: ρ ↦ ΣLρL†.

Equations

• CSD.LF6.jumpCLM L = ∑ k : ι, CSD.LF6.mulLeftCLM (L k) * CSD.LF6.mulRightCLM (L k).conjTranspose

theorem CSD.LF6.driftCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (ρ : Matrix n n ℂ) : (driftCLM H L) ρ = gkslG H L * ρ + ρ * (gkslG H L).conjTranspose

theorem CSD.LF6.jumpCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (L : ι → Matrix n n ℂ) (ρ : Matrix n n ℂ) : (jumpCLM L) ρ = ∑ k : ι, L k * ρ * (L k).conjTranspose

theorem CSD.LF6.lindbladGeneratorCLM_split {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {H : Matrix n n ℂ} (hH : H.IsHermitian) (L : ι → Matrix n n ℂ) : lindbladGeneratorCLM H L = driftCLM H L + jumpCLM L

The drift/jump split (Hermitian H): the GKSL generator is the drift conjugation plus the Kraus jump part.

The two flows are positive

theorem CSD.LF6.exp_smul_driftCLM_apply {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) (ρ : Matrix n n ℂ) : (NormedSpace.exp (t • driftCLM H L)) ρ = NormedSpace.exp (t • gkslG H L) * ρ * NormedSpace.exp (t • (gkslG H L).conjTranspose)

The drift flow is conjugation: e^{t·drift} ρ = e^{tG} ρ e^{tG†}.

theorem CSD.LF6.exp_smul_driftCLM_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : ((NormedSpace.exp (t • driftCLM H L)) ρ).PosSemidef

The drift flow is positive at every time — it is conjugation by e^{tG}.

theorem CSD.LF6.jumpCLM_posSemidef_apply {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (L : ι → Matrix n n ℂ) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : ((jumpCLM L) ρ).PosSemidef

The jump part preserves positive semidefiniteness (the generator-tier Choi–Kraus witness, at the endomorphism level).

theorem CSD.LF6.smul_jumpCLM_pow_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (L : ι → Matrix n n ℂ) {t : ℝ} (ht : 0 ≤ t) (m : ℕ) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : (((t • jumpCLM L) ^ m) ρ).PosSemidef

Powers of the scaled jump part preserve positive semidefiniteness.

theorem CSD.LF6.exp_smul_jumpCLM_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (L : ι → Matrix n n ℂ) {t : ℝ} (ht : 0 ≤ t) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : ((NormedSpace.exp (t • jumpCLM L)) ρ).PosSemidef

The jump flow is positive for t ≥ 0: every term of the exponential series is PSD, and PSD passes to the limit.

Assembly: the semigroup is positive

theorem CSD.LF6.step_pow_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) {u : ℝ} (hu : 0 ≤ u) (k : ℕ) {ρ : Matrix n n ℂ} (hρ : ρ.PosSemidef) : (((NormedSpace.exp (u • driftCLM H L) * NormedSpace.exp (u • jumpCLM L)) ^ k) ρ).PosSemidef

Powers of one Trotter step preserve positive semidefiniteness.

theorem CSD.LF6.matrix_nontrivial {n : Type u_1} [DecidableEq n] [Nonempty n] : Nontrivial (Matrix n n ℂ)

Matrix space over a nonempty index is nontrivial.

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

★★ The Lindblad semigroup is a positive map: for every GKSL generator with Hermitian H and every t ≥ 0, Φₜ = e^{tℒ} maps positive semidefinite matrices to positive semidefinite matrices. The half LF6/LindbladSemigroup.lean deferred as out of Mathlib's reach, closed by the Banach-algebra Trotter formula over the two positive flows.

theorem CSD.LF6.lindbladSemigroup_amplified_posSemidef {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {m' : Type u_3} [Fintype m'] [DecidableEq m'] [Nonempty m'] [Nonempty n] {H : Matrix n n ℂ} (hH : H.IsHermitian) (L : ι → Matrix n n ℂ) {t : ℝ} (ht : 0 ≤ t) {ρ : Matrix (m' × n) (m' × n) ℂ} (hρ : ρ.PosSemidef) : ((lindbladSemigroup (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 H) (fun (k : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (L k)) t) ρ).PosSemidef

★ The complete-positivity shape: the amplified generator (1 ⊗ H, 1 ⊗ Lₖ) is itself GKSL with Hermitian Hamiltonian, so positivity survives every ancilla amplification of the generator — a literal instantiation of lindbladSemigroup_posSemidef on the product index.

The id ⊗ Φ identification (Q23)

The amplified generator's flow IS id ⊗ Φₜ: the flow of (1 ⊗ H, 1 ⊗ Lₖ) acts on each ancilla block of the composite matrix by Φₜ separately. With this, lindbladSemigroup_amplified_posSemidef is complete positivity of Φₜ in so many words (lindbladSemigroup_completelyPositive).

noncomputable def CSD.LF6.blockAtCLM {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] (i j : m') : Matrix (m' × n) (m' × n) ℂ →L[ℝ] Matrix n n ℂ

The (i,j) ancilla block of a composite matrix, as a continuous ℝ-linear map: blockAtCLM i j M k l = M (i,k) (j,l).

Equations

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

@[simp]

theorem CSD.LF6.blockAtCLM_apply_entry {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] (i j : m') (M : Matrix (m' × n) (m' × n) ℂ) (k l : n) : (blockAtCLM i j) M k l = M (i, k) (j, l)

theorem CSD.LF6.blockAtCLM_csmul {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] (i j : m') (c : ℂ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) (c • M) = c • (blockAtCLM i j) M

blockAtCLM commutes with complex scaling (it is ℝ-bundled but ℂ-linear as a function).

theorem CSD.LF6.blockAtCLM_one_kronecker_mul {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (i j : m') (A : Matrix n n ℂ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 A * M) = A * (blockAtCLM i j) M

Left Kronecker collapse: multiplying by 1 ⊗ A on the left acts on each ancilla block by left multiplication by A.

theorem CSD.LF6.blockAtCLM_mul_one_kronecker {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (i j : m') (B : Matrix n n ℂ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) (M * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B) = (blockAtCLM i j) M * B

Right Kronecker collapse: multiplying by 1 ⊗ B on the right acts on each ancilla block by right multiplication by B.

theorem CSD.LF6.blockAtCLM_ampDissipator {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (i j : m') (L : Matrix n n ℂ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) (lindbladDissipator (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 L) M) = lindbladDissipator L ((blockAtCLM i j) M)

The amplified dissipator acts blockwise.

theorem CSD.LF6.blockAtCLM_ampGenerator {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (i j : m') (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) ((lindbladGeneratorCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 H) fun (k : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (L k)) M) = (lindbladGeneratorCLM H L) ((blockAtCLM i j) M)

★ The amplified generator acts blockwise: the GKSL generator of (1 ⊗ H, 1 ⊗ Lₖ) applied to a composite matrix is the GKSL generator of (H, Lₖ) applied to each ancilla block. No Hermiticity is needed — this is pure Kronecker algebra.

theorem CSD.LF6.blockAtCLM_smul_ampGen_pow {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (i j : m') (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) (p : ℕ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) (((t • lindbladGeneratorCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 H) fun (k : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (L k)) ^ p) M) = ((t • lindbladGeneratorCLM H L) ^ p) ((blockAtCLM i j) M)

Powers of the scaled amplified generator act blockwise.

theorem CSD.LF6.blockAtCLM_lindbladSemigroup_amplified {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (i j : m') (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) (M : Matrix (m' × n) (m' × n) ℂ) : (blockAtCLM i j) ((lindbladSemigroup (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 H) (fun (k : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (L k)) t) M) = (lindbladSemigroup H L t) ((blockAtCLM i j) M)

★★ The amplified flow acts blockwise — the block form of id ⊗ Φₜ: the Lindblad semigroup of (1 ⊗ H, 1 ⊗ Lₖ) applied to a composite matrix is Φₜ applied to each ancilla block. Exponential-series transport of blockAtCLM_ampGenerator through expCLM_apply_hasSum.

noncomputable def CSD.LF6.idTensorCLM {n : Type u_1} [Fintype n] (m' : Type u_4) [Fintype m'] [DecidableEq m'] (Φ : Matrix n n ℂ →L[ℝ] Matrix n n ℂ) : Matrix (m' × n) (m' × n) ℂ →L[ℝ] Matrix (m' × n) (m' × n) ℂ

id ⊗ Φ: the ancilla amplification of a superoperator, acting on each ancilla block of the composite matrix by Φ separately — (idTensorCLM m' Φ) M (i,k) (j,l) = Φ (blockAtCLM i j M) k l.

Equations

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

@[simp]

theorem CSD.LF6.idTensorCLM_apply_entry {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (Φ : Matrix n n ℂ →L[ℝ] Matrix n n ℂ) (M : Matrix (m' × n) (m' × n) ℂ) (p q : m' × n) : (idTensorCLM m' Φ) M p q = Φ ((blockAtCLM p.1 q.1) M) p.2 q.2

theorem CSD.LF6.idTensorCLM_one {n : Type u_1} [Fintype n] {m' : Type u_3} [Fintype m'] [DecidableEq m'] : idTensorCLM m' 1 = 1

Amplifying the identity gives the identity: the blocks reassemble.

theorem CSD.LF6.idTensor_lindbladSemigroup {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {m' : Type u_3} [Fintype m'] [DecidableEq m'] (H : Matrix n n ℂ) (L : ι → Matrix n n ℂ) (t : ℝ) : idTensorCLM m' (lindbladSemigroup H L t) = lindbladSemigroup (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 H) (fun (k : ι) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (L k)) t

★★ The identification: id ⊗ Φₜ IS the flow of the amplified generator (1 ⊗ H, 1 ⊗ Lₖ) — as an equality of superoperators on the composite matrix space. This is the lemma that lets lindbladSemigroup_amplified_posSemidef be cited as complete positivity of Φₜ in so many words.

theorem CSD.LF6.lindbladSemigroup_completelyPositive {n : Type u_1} [Fintype n] [DecidableEq n] {ι : Type u_2} [Fintype ι] {m' : Type u_3} [Fintype m'] [DecidableEq m'] [Nonempty m'] [Nonempty n] {H : Matrix n n ℂ} (hH : H.IsHermitian) (L : ι → Matrix n n ℂ) {t : ℝ} (ht : 0 ≤ t) {ρ : Matrix (m' × n) (m' × n) ℂ} (hρ : ρ.PosSemidef) : ((idTensorCLM m' (lindbladSemigroup H L t)) ρ).PosSemidef

★★ The Lindblad semigroup is completely positive — in so many words: for every GKSL generator with Hermitian H, every t ≥ 0, and every finite ancilla, id ⊗ Φₜ maps positive semidefinite composite matrices to positive semidefinite composite matrices. The identification rewrites the claim onto lindbladSemigroup_amplified_posSemidef.