Conditions EQ-MEAS, EQ-LIND, EQ-HS, EQ-KL on a black-box process $\Phi_X$

Definition

pme_measurement_conditions

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

lindbladprojective-measurementquantum-mechanicsrelative-entropy

The four characterizations of the spectral equilibration process $\Phi_X$ associated with a Hermitian observable $X=\sum_x xP_x$ on $\mathbb C^n$ , as properties of a map $\Phi$ on matrices (only its values on density matrices matter).

EQ-MEAS (nonselective projective measurement): $\Phi(\rho)=\sum_x P_x\rho P_x$ for every density matrix $\rho$ .
EQ-LIND (spectral equilibration): for every density matrix $\rho$ , the Lindblad equation $\frac{d\rho}{dt}=X\rho X-\tfrac12\{X^2,\rho\}$ with $\rho(0)=\rho$ has a solution on $t\ge0$ , and $\Phi(\rho)=\lim_{t\to\infty}\rho(t)$ for every such solution.
EQ-HS (closest commuting ensemble): for every density matrix $\rho$ , $\Phi(\rho)$ is a density matrix with $[\Phi(\rho),X]=0$ attaining $\min\{\|\rho-\sigma\|_{HS}^2:\sigma\in D,\ [\sigma,X]=0\}$ .
EQ-KL (closest commuting ensemble in information): the same with the relative entropy $D(\rho\|\sigma)$ in place of $\|\rho-\sigma\|_{HS}^2$ .

Here $\Phi(\rho)=\operatorname{argmin}$ is encoded as " $\Phi(\rho)$ is a minimizer"; uniqueness of the minimizer is part of what Theorem 1 proves.

Definition code

import Mathlib
import Definitions.Def_pme_quantum_basics

/-!
The four characterizations EQ-MEAS, EQ-LIND, EQ-HS, EQ-KL of the black-box spectral
equilibration process `Φ_X` (Carcassi, AoP brief 017, Section 2), as predicates on a map
`Φ : Matrix n n ℂ → Matrix n n ℂ` (only its values on density matrices matter).
-/

namespace ProjectiveMeasurementEquilibration

open Matrix Filter Topology

variable {n : Type} [Fintype n] [DecidableEq n]

/-- Condition EQ-MEAS: `Φ(ρ) = ∑ₓ Pₓ ρ Pₓ` for every density matrix `ρ`. -/
def EqMeas {X : Matrix n n ℂ} (hX : X.IsHermitian) (Φ : Matrix n n ℂ → Matrix n n ℂ) : Prop :=
  ∀ ρ, IsDensityMatrix ρ → Φ ρ = pinching hX ρ

/-- Condition EQ-LIND: for every density matrix `ρ`, the Lindblad equation
`dρ/dt = XρX − ½{X², ρ}` started at `ρ` has a solution on `t ≥ 0`, and every such solution
converges to `Φ(ρ)` as `t → ∞`. -/
def EqLind (X : Matrix n n ℂ) (Φ : Matrix n n ℂ → Matrix n n ℂ) : Prop :=
  ∀ ρ, IsDensityMatrix ρ →
    (∃ ρt : ℝ → Matrix n n ℂ, IsLindbladSolution X ρ ρt) ∧
    ∀ ρt : ℝ → Matrix n n ℂ, IsLindbladSolution X ρ ρt → Tendsto ρt atTop (𝓝 (Φ ρ))

/-- Condition EQ-HS: `Φ(ρ)` is a density matrix commuting with `X` that minimizes
`‖ρ − σ‖²_HS` over all density matrices `σ` commuting with `X`. -/
def EqHS (X : Matrix n n ℂ) (Φ : Matrix n n ℂ → Matrix n n ℂ) : Prop :=
  ∀ ρ, IsDensityMatrix ρ →
    IsDensityMatrix (Φ ρ) ∧ X * Φ ρ = Φ ρ * X ∧
    ∀ σ, IsDensityMatrix σ → X * σ = σ * X → hsDistSq ρ (Φ ρ) ≤ hsDistSq ρ σ

/-- Condition EQ-KL: `Φ(ρ)` is a density matrix commuting with `X` that minimizes
`D(ρ‖σ)` over all density matrices `σ` commuting with `X`. -/
def EqKL (X : Matrix n n ℂ) (Φ : Matrix n n ℂ → Matrix n n ℂ) : Prop :=
  ∀ ρ, IsDensityMatrix ρ →
    IsDensityMatrix (Φ ρ) ∧ X * Φ ρ = Φ ρ * X ∧
    ∀ σ, IsDensityMatrix σ → X * σ = σ * X → relEntropy ρ (Φ ρ) ≤ relEntropy ρ σ

end ProjectiveMeasurementEquilibration

Source

G. Carcassi (Assumptions of Physics collaboration), "Projective measurements are equilibration processes", AoP Technical Brief 017, https://assumptionsofphysics.org/resources/briefs, Section 2, Conditions EQ-MEAS, EQ-LIND, EQ-HS, EQ-KL, p. 2

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 a finite index type $n$ , a matrix $X\in M_n(\mathbb C)$ and an arbitrary function $\Phi:M_n(\mathbb C)\to M_n(\mathbb C)$ , four propositions are defined (all using the notions of the companion basics file). In each, $\rho$ and $\sigma$ range over all density matrices (positive semidefinite, trace $1$ ).

$\mathrm{EqMeas}$ (takes a proof $h_X$ that $X$ is Hermitian): for every density matrix $\rho$ , $\Phi(\rho)=\sum_{x}P_x\rho P_x$ , the sum over the distinct eigenvalues of $X$ , $P_x$ the eigenprojections.
$\mathrm{EqLind}$ : for every density matrix $\rho$ , (a) there exists a function $\rho(\cdot):\mathbb R\to M_n(\mathbb C)$ with $\rho(0)=\rho$ and right-sided/within- $[0,\infty)$ derivative $\rho'(t)=X\rho(t)X-\tfrac12(X^2\rho(t)+\rho(t)X^2)$ for all $t\ge 0$ ; and (b) every such function satisfies $\rho(t)\to\Phi(\rho)$ entrywise as $t\to+\infty$ .
$\mathrm{EqHS}$ : for every density matrix $\rho$ : $\Phi(\rho)$ is a density matrix, $X\Phi(\rho)=\Phi(\rho)X$ , and for every density matrix $\sigma$ with $X\sigma=\sigma X$ , $\sum_{ij}|\rho_{ij}-\Phi(\rho)_{ij}|^2\le\sum_{ij}|\rho_{ij}-\sigma_{ij}|^2$ .
$\mathrm{EqKL}$ : the same as 3 but with the inequality $D(\rho\|\Phi(\rho))\le D(\rho\|\sigma)$ in the extended reals, where $D(\rho\|\sigma)=\operatorname{Re}\operatorname{tr}(\rho(\log\rho-\log\sigma))$ when $\ker\sigma\subseteq\ker\rho$ and $+\infty$ otherwise ( $\log$ by functional calculus with $\log 0=0$ ).

Only $\mathrm{EqMeas}$ refers to the Hermitian proof; the others take $X$ alone. None constrains $\Phi$ outside density matrices. If $n$ is empty all four 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

Conditions EQ-MEAS, EQ-LIND, EQ-HS, EQ-KL on a black-box process ΦX\Phi_XΦX​

Conditions EQ-MEAS, EQ-LIND, EQ-HS, EQ-KL on a black-box process $\Phi_X$