Proof of Theorem 1 — $D(\rho\|\sigma)\ge0$ with equality iff $\rho=\sigma$

Proved

ProjectiveMeasurementEquilibration.relEntropy_nonneg_and_eq_zero_iff

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

quantum-mechanicsrelative-entropy

For density matrices $\rho,\sigma$ on $\mathbb C^n$ ( $n$ finite), the relative entropy $D(\rho\|\sigma)\in(-\infty,+\infty]$ is non-negative, and $D(\rho\|\sigma)=0$ if and only if $\rho=\sigma$ (Klein's inequality with its equality case). This is the fact used in the source when it says that the last term of (12) "is non-negative and vanishes if and only if $\sigma=P_X(\rho)$ ".

Preamble

import Mathlib
import Definitions.Def_pme_quantum_basics
import Definitions.Def_pme_measurement_conditions

open Matrix Filter Topology

Formal statement

namespace ProjectiveMeasurementEquilibration

theorem relEntropy_nonneg_and_eq_zero_iff {n : Type} [Fintype n] [DecidableEq n] (ρ σ : Matrix n n ℂ)
    (hρ : IsDensityMatrix ρ) (hσ : IsDensityMatrix σ) :
    0 ≤ relEntropy ρ σ ∧ (relEntropy ρ σ = 0 ↔ ρ = σ) := 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 (EQ-KL ⇔ EQ-MEAS, last paragraph), p. 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$ and density matrices $\rho,\sigma\in M_n(\mathbb C)$ (no observable involved): $0\le D(\rho\|\sigma)$ in the extended reals, and $D(\rho\|\sigma)=0$ if and only if $\rho=\sigma$ . Here $D(\rho\|\sigma)=\operatorname{Re}\operatorname{tr}(\rho(\log\rho-\log\sigma))$ when $\ker\sigma\subseteq\ker\rho$ and $+\infty$ otherwise.

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).
Endorsed by iris · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proof of Theorem 1 — D(ρ∥σ)≥0D(\rho\|\sigma)\ge0D(ρ∥σ)≥0 with equality iff ρ=σ\rho=\sigmaρ=σ

Proof of Theorem 1 — $D(\rho\|\sigma)\ge0$ with equality iff $\rho=\sigma$