Prove2Me

The Lindblad generator with jump operator a†a^\dagger on anti-normal monomials

Proved
HighEntropyLimit.lindblad_antinormal_monomial

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-mechanics

Let A\mathcal A be a C\mathbb C-algebra containing a,a†a, a^\dagger with aa†−a†a=1aa^\dagger - a^\dagger a = 1. Let γ∈R\gamma\in\mathbb R and n,m∈Nn,m\in\mathbb N. The Heisenberg-picture Lindblad generator with H=0H = 0 and a single jump operator L=a†L = a^\dagger (so L†=aL^\dagger = a) acts on anti-normally ordered monomials by

L(an(a†)m)=γ2(n+m) an(a†)m.\mathcal L\big(a^n(a^\dagger)^m\big) = \frac{\gamma}{2}(n+m)\,a^n(a^\dagger)^m.

Integrating gives (an(a†)m)(t)=(λ)n+man(a†)m(a^n(a^\dagger)^m)(t) = (\sqrt\lambda)^{n+m}a^n(a^\dagger)^m with λ=eγt\lambda = e^{\gamma t}.

Formalization Note The value of ℏ\hbar is irrelevant here because H=0H=0.

Preamble
import Mathlib
import Definitions.Def_HighEntropyLimit_lindblad
Formal statement
namespace HighEntropyLimit
theorem lindblad_antinormal_monomial {A : Type*} [Ring A] [Algebra ℂ A] (a adag : A)
    (hccr : a * adag - adag * a = 1) (hbar γ : ℝ) (n m : ℕ) :
    lindbladHeisenberg hbar 0 [(γ, adag, a)] (a ^ n * adag ^ m) =
      ((γ / 2 * (n + m) : ℝ) : ℂ) • (a ^ n * adag ^ m) := by sorry
end HighEntropyLimit
Source
Carcassi, Landini, Aidala, Classical mechanics as the high-entropy limit of quantum mechanics, arXiv:2411.00972v3 (1 Feb 2026), https://arxiv.org/abs/2411.00972, p. 9, Eqs. (26)-(28), with γ_i = {γ}, L_i = {a†}, H = 0
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph