Theorem 1 — EQ-MEAS, EQ-LIND, EQ-HS, EQ-KL are equivalent (finite dimension)

Proved

ProjectiveMeasurementEquilibration.projective_measurement_equilibration

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

lindbladprojective-measurementquantum-mechanicsrelative-entropy

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$ . Let $\Phi$ be any map on matrices (the black-box spectral equilibration process $\Phi_X$ ; only its values on density matrices matter). Then the conditions

EQ-MEAS: $\Phi(\rho)=\sum_xP_x\rho P_x$ ;
EQ-LIND: $\Phi(\rho)=\lim_{t\to\infty}\rho(t)$ , where $\frac{d\rho}{dt}=X\rho X-\tfrac12\{X^2,\rho\}$ , $\rho(0)=\rho$ ;
EQ-HS: $\Phi(\rho)=\operatorname{argmin}_{\sigma\in D,\,[\sigma,X]=0}\|\rho-\sigma\|_{HS}^2$ ;
EQ-KL: $\Phi(\rho)=\operatorname{argmin}_{\sigma\in D,\,[\sigma,X]=0}D(\rho\|\sigma)$ ,

each required for all density matrices $\rho$ , are pairwise equivalent. This is Theorem 1 of the source specialised to finite-dimensional Hilbert spaces, where Condition [B]FINENT holds automatically.

Preamble

import Mathlib
import Definitions.Def_pme_quantum_basics
import Definitions.Def_pme_measurement_conditions

open Matrix Filter Topology

Formal statement

namespace ProjectiveMeasurementEquilibration

theorem projective_measurement_equilibration {n : Type} [Fintype n] [DecidableEq n] {X : Matrix n n ℂ}
    (hX : X.IsHermitian) (Φ : Matrix n n ℂ → Matrix n n ℂ) :
    (EqMeas hX Φ ↔ EqLind X Φ) ∧ (EqMeas hX Φ ↔ EqHS X Φ) ∧ (EqMeas hX Φ ↔ EqKL X Φ) := 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, Theorem 1, p. 2 (proof pp. 2–4)

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$ , every Hermitian matrix $X\in M_n(\mathbb C)$ and every function $\Phi:M_n(\mathbb C)\to M_n(\mathbb C)$ , the three equivalences hold: $\mathrm{EqMeas}\iff\mathrm{EqLind}$ , $\mathrm{EqMeas}\iff\mathrm{EqHS}$ , and $\mathrm{EqMeas}\iff\mathrm{EqKL}$ , where (all quantifiers over density matrices = positive semidefinite trace-one matrices):

$\mathrm{EqMeas}$ : $\Phi(\rho)=\sum_{x\in\Lambda}P_x\rho P_x$ for all $\rho$ ( $\Lambda$ distinct eigenvalues of $X$ , $P_x$ eigenprojections);
$\mathrm{EqLind}$ : for all $\rho$ , a function $\rho(\cdot):\mathbb R\to M_n(\mathbb C)$ with $\rho(0)=\rho$ and $\rho'(t)=X\rho(t)X-\tfrac12(X^2\rho(t)+\rho(t)X^2)$ within $[0,\infty)$ for $t\ge0$ exists, and every such function tends entrywise to $\Phi(\rho)$ as $t\to\infty$ ;
$\mathrm{EqHS}$ : for all $\rho$ , $\Phi(\rho)$ is a density matrix commuting with $X$ and $\sum_{ij}|\rho_{ij}-\Phi(\rho)_{ij}|^2\le\sum_{ij}|\rho_{ij}-\sigma_{ij}|^2$ for every density matrix $\sigma$ commuting with $X$ ;
$\mathrm{EqKL}$ : as $\mathrm{EqHS}$ but with $D(\rho\|\Phi(\rho))\le D(\rho\|\sigma)$ , $D$ the extended-real relative entropy ( $+\infty$ unless $\ker\sigma\subseteq\ker\rho$ , otherwise $\operatorname{Re}\operatorname{tr}(\rho(\log\rho-\log\sigma))$ with $\log0=0$ ).

The statement is only about finite-dimensional matrices; separable infinite-dimensional Hilbert spaces and unbounded observables are not covered. When $n$ is empty, all four conditions hold vacuously.

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