Theorem 1, p. 2 — characterization of pure stationary states

Proved

DissipativePrep.Unique.theorem_1

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

dissipative-state-preparationlindblad-master-equationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1stationary-state

Let $\mathcal L$ be the Liouvillian of Eq. (2) with Hermitian Hamiltonian $H$ , jump operators $c_1,\dots,c_m$ and rates $g_l>0$ , and write $P = \sum_l g_l c_l^\dagger c_l$ , $Q = P - iH$ . Let $|\Phi\rangle$ be a unit vector. Then $\mathcal L(|\Phi\rangle\langle\Phi|) = 0$ if and only if

$Q^\dagger|\Phi\rangle = \lambda|\Phi\rangle$ for some $\lambda\in\mathbb C$ , and
$c_l|\Phi\rangle = \lambda_l|\Phi\rangle$ for every $l$ , for some $\lambda_l\in\mathbb C$ with

\sum_l g_l\,|\lambda_l|^2 = \operatorname{Re}(\lambda).

The theorem reduces stationarity of a pure state to a common-eigenvector condition on the jump operators, which is the basis of the construction in §IV.

Formalization Note The page allows $g_l\ge 0$ ; with $g_l = 0$ the operator $c_l$ does not enter $\mathcal L$ and condition 2 can fail, so $g_l>0$ is assumed. $|\Phi\rangle$ is required to be a unit vector (a state).

Preamble

import Mathlib
import Definitions.Def_DissipativePrep_Unique_Model

open scoped Matrix ComplexConjugate
open QAlgorithms QAlgorithms.Papers.Independent.Dependency50.P16

Formal statement

namespace DissipativePrep.Unique

theorem theorem_1 {d m : ℕ} (H : Matrix (Fin d) (Fin d) ℂ) (hH : H.IsHermitian)
    (c : Fin m → Matrix (Fin d) (Fin d) ℂ) (g : Fin m → ℝ) (hg : ∀ l, 0 < g l)
    (Φ : EuclideanSpace ℂ (Fin d)) (hΦ : ‖Φ‖ = 1) :
    gkslGenerator (krausData H hH c g) (pureDensity Φ) = 0 ↔
      ∃ lam : ℂ, act (Qop H c g)ᴴ Φ = lam • Φ ∧
        ∃ lamL : Fin m → ℂ, (∀ l, act (c l) Φ = lamL l • Φ) ∧
          ∑ l, g l * ‖lamL l‖ ^ 2 = lam.re := by sorry

end DissipativePrep.Unique

Source

Kraus et al., Preparation of entangled states by quantum Markov processes, arXiv:0803.1463v3, p. 2, Theorem 1

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph