Prove2Me

Eqs. (4)–(5) — Lindblad blocks decay as e−t(x−y)2/2e^{-t(x-y)^2/2}

Proved
ProjectiveMeasurementEquilibration.lindblad_block_solution

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

lindbladquantum-mechanics

Throughout, nn is a finite index type, the Hilbert space is Cn\mathbb C^n, XX is a Hermitian n×nn\times n complex matrix with spectral decomposition X=∑xx PxX=\sum_{x} x\,P_x (xx ranging over the distinct eigenvalues, PxP_x the orthogonal projection onto the xx-eigenspace, and Px=0P_x=0 for xx not an eigenvalue), and a density matrix is a positive semidefinite matrix of trace 11. Let ρ(t)\rho(t), t≥0t\ge0, be any solution of the Lindblad equation

dρdt=XρX−12{X2,ρ},ρ(0)=ρ.\frac{d\rho}{dt}=X\rho X-\tfrac12\{X^2,\rho\},\qquad \rho(0)=\rho.

Then for all t≥0t\ge 0 and all real x,yx,y,

Px ρ(t) Py=e−t2(x−y)2 Px ρ(0) Py.P_x\,\rho(t)\,P_y=e^{-\frac t2(x-y)^2}\,P_x\,\rho(0)\,P_y.

In particular diagonal blocks are constant and off-diagonal blocks decay exponentially.

Preamble
import Mathlib
import Definitions.Def_pme_quantum_basics
import Definitions.Def_pme_measurement_conditions

open Matrix Filter Topology
Formal statement
namespace ProjectiveMeasurementEquilibration

theorem lindblad_block_solution {n : Type} [Fintype n] [DecidableEq n] {X : Matrix n n ℂ} (hX : X.IsHermitian)
    (ρ : Matrix n n ℂ) (ρt : ℝ → Matrix n n ℂ) (hsol : IsLindbladSolution X ρ ρt)
    (t : ℝ) (ht : 0 ≤ t) (x y : ℝ) :
    eigenproj hX x * ρt t * eigenproj hX y =
      ((Real.exp (-(t / 2) * (x - y) ^ 2) : ℝ) : ℂ) • (eigenproj hX x * ρ * eigenproj hX y) := by sorry

end ProjectiveMeasurementEquilibration
Source
G. Carcassi (Assumptions of Physics collaboration), "Projective measurements are equilibration processes", AoP Technical Brief 017, https://assumptionsofphysics.org/resources/briefs, proof of Theorem 1, eqs. (3)–(5), pp. 2–3
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as the drafter; non-blind

Non-blind read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, at the explicit request of the account owner. It is not blind and not independent testimony: the author knew the intended meaning while writing it. Reviewers should not treat it as an independent audit.

For every finite index type nn, Hermitian X∈Mn(C)X\in M_n(\mathbb C), matrix ρ∈Mn(C)\rho\in M_n(\mathbb C) (arbitrary, not necessarily a density matrix), and function ρ(⋅):R→Mn(C)\rho(\cdot):\mathbb R\to M_n(\mathbb C) such that ρ(0)=ρ\rho(0)=\rho and, for each t≥0t\ge0, ρ(⋅)\rho(\cdot) has derivative within [0,∞)[0,\infty) at tt equal to Xρ(t)X−12(X2ρ(t)+ρ(t)X2)X\rho(t)X-\tfrac12(X^2\rho(t)+\rho(t)X^2): for every t≥0t\ge0 and all real numbers x,yx,y,

Px ρ(t) Py=e−t2(x−y)2  Px ρ Py,P_x\,\rho(t)\,P_y=e^{-\frac t2 (x-y)^2}\;P_x\,\rho\,P_y,

where PxP_x is the eigenprojection of XX for xx (the zero matrix if xx is not an eigenvalue, in which case both sides vanish). The real exponential is cast to a complex scalar.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

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

View graph