Eqs. (9)–(10) — Lindblad evolution converges to $\mathcal P_X(\rho)$

Proved

ProjectiveMeasurementEquilibration.lindblad_tendsto_pinching

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

lindbladpinchingquantum-mechanics

Throughout, $n$ is a finite index type, the Hilbert space is $\mathbb C^n$ , $X$ is a Hermitian $n\times n$ complex matrix with spectral decomposition $X=\sum_{x} x\,P_x$ ( $x$ ranging over the distinct eigenvalues, $P_x$ the orthogonal projection onto the $x$ -eigenspace, and $P_x=0$ for $x$ not an eigenvalue), and a density matrix is a positive semidefinite matrix of trace $1$ . For every density matrix $\rho$ , the Lindblad equation $\frac{d\rho}{dt}=X\rho X-\tfrac12\{X^2,\rho\}$ with initial value $\rho$ has a solution on $t\ge 0$ , and every such solution satisfies

\lim_{t\to\infty}\rho(t)=\mathcal P_X(\rho)=\sum_xP_x\rho P_x.

(In finite dimension all matrix norms, including the trace norm and the Hilbert–Schmidt norm, induce the entrywise topology used here.)

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_tendsto_pinching {n : Type} [Fintype n] [DecidableEq n] {X : Matrix n n ℂ} (hX : X.IsHermitian)
    (ρ : Matrix n n ℂ) (hρ : IsDensityMatrix ρ) :
    (∃ ρt : ℝ → Matrix n n ℂ, IsLindbladSolution X ρ ρt) ∧
    ∀ ρt : ℝ → Matrix n n ℂ, IsLindbladSolution X ρ ρt →
      Tendsto ρt atTop (𝓝 (pinching hX ρ)) := 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. (6)–(10), p. 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 $n$ , Hermitian $X\in M_n(\mathbb C)$ and density matrix $\rho$ (positive semidefinite, trace $1$ ), two things hold:

(a) there exists a function $\rho(\cdot):\mathbb R\to M_n(\mathbb C)$ with $\rho(0)=\rho$ whose derivative within $[0,\infty)$ at every $t\ge0$ equals $X\rho(t)X-\tfrac12(X^2\rho(t)+\rho(t)X^2)$ ;

(b) every such function converges, entrywise as $t\to+\infty$ , to

\sum_{x\in\Lambda}P_x\rho P_x,

$\Lambda$ the set of distinct eigenvalues of $X$ and $P_x$ the eigenprojections.

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

Eqs. (9)–(10) — Lindblad evolution converges to PX(ρ)\mathcal P_X(\rho)PX​(ρ)

Eqs. (9)–(10) — Lindblad evolution converges to $\mathcal P_X(\rho)$