Theorem 5 (Wall 2013): eigenvalue majorization under positive unital trace-preserving maps

Proved

WallGSL.unital_positive_map_eigenvalue_majorization

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

majorizationmatrix-analysisquantum-information

Theorem 5 (appendix). Let $\rho$ be an $n\times n$ density matrix (positive semidefinite, trace $1$ ) and let $T$ be a linear map on $n\times n$ complex matrices that is positive (maps positive semidefinite matrices to positive semidefinite matrices), trace preserving and identity preserving ( $T(I)=I$ ). Then for every $i$ , the sum of the $i$ largest eigenvalues of $T(\rho)$ is at most the sum of the $i$ largest eigenvalues of $\rho$ :

\sum_{j=1}^{i}\lambda^{\downarrow}_j\big(T(\rho)\big)\ \le\ \sum_{j=1}^{i}\lambda^{\downarrow}_j(\rho).

In the paper's notation, $\operatorname{tr}(Q\,T(\rho)\,Q)\le\operatorname{tr}(P\rho P)$ , where $P$ and $Q$ project onto the eigenspaces of the $i$ largest eigenvalues of $\rho$ and of $T(\rho)$ .

This is the statement that probability eigenvalues can only evolve towards equalization, which underlies the coarse-grained second law discussed in §2.1.

Formalization Note "The sum of the $i$ largest eigenvalues" is expressed without sorting: every sum of $i$ eigenvalues of $T(\rho)$ (indexed by a set $s$ of size $i$ ) is bounded by some sum of $i$ eigenvalues of $\rho$ .

Preamble

import Mathlib

open Matrix
open scoped ComplexOrder

Formal statement

namespace WallGSL

/-- Theorem 5 (appendix) of Wall (2013): a trace-preserving, identity-preserving, positive
linear map `T` on `n × n` complex matrices can only equalize the eigenvalues of a density
matrix `ρ`: for every `i`, the sum of any `i` eigenvalues of `T ρ` is at most the sum of
the `i` largest eigenvalues of `ρ`. -/
theorem unital_positive_map_eigenvalue_majorization
    {n : ℕ} (T : Matrix (Fin n) (Fin n) ℂ →ₗ[ℂ] Matrix (Fin n) (Fin n) ℂ)
    (hT_pos : ∀ A : Matrix (Fin n) (Fin n) ℂ, A.PosSemidef → (T A).PosSemidef)
    (hT_trace : ∀ A : Matrix (Fin n) (Fin n) ℂ, (T A).trace = A.trace)
    (hT_one : T 1 = 1)
    (ρ : Matrix (Fin n) (Fin n) ℂ) (hρ : ρ.PosSemidef) (hρ_tr : ρ.trace = 1)
    (i : ℕ) (s : Finset (Fin n)) (hs : s.card = i) :
    ∃ t : Finset (Fin n), t.card = i ∧
      ∑ j ∈ s, (hT_pos ρ hρ).isHermitian.eigenvalues j ≤ ∑ j ∈ t, hρ.isHermitian.eigenvalues j := by sorry

end WallGSL

Source

A. C. Wall, The generalized second law implies a quantum singularity theorem, Class. Quantum Grav. 30 (2013) 165003, https://doi.org/10.1088/0264-9381/30/16/165003, Appendix, Theorem 5 eq. (A.3), p. 31

Read-back

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

Provenance note — this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It is therefore not independent testimony and must not be mistaken for a blind audit; reviewers should treat it as the drafter's own literal reading of the code and compare it against the source themselves.

Data. A natural number $n$ ; a $\mathbb C$ -linear map $T$ from $n\times n$ complex matrices to $n\times n$ complex matrices; an $n\times n$ complex matrix $\rho$ ; a natural number $i$ ; and a set $s\subseteq\{1,\dots,n\}$ .

Hypotheses.

$T(A)$ is positive semidefinite whenever $A$ is positive semidefinite (Hermitian with $x^*Ax\ge0$ for all $x$ );
$\operatorname{tr}T(A)=\operatorname{tr}A$ for every matrix $A$ ;
$T(I)=I$ ;
$\rho$ is positive semidefinite and $\operatorname{tr}\rho=1$ ;
$|s|=i$ .

Conclusion. Writing $\mu_1,\dots,\mu_n$ for the eigenvalues of the Hermitian matrix $T(\rho)$ and $\lambda_1,\dots,\lambda_n$ for those of $\rho$ (each listed with multiplicity, in the order chosen by Mathlib's spectral theorem), there is a set $t\subseteq\{1,\dots,n\}$ with $|t|=i$ and

\sum_{j\in s}\mu_j\ \le\ \sum_{j\in t}\lambda_j.

If $i>n$ there is no such $s$ and the statement is vacuous; for $i=0$ it reads $0\le 0$ . Complete positivity of $T$ is not assumed.

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