Von Neumann's trace inequality for Hermitian matrices: $\operatorname{Re}\operatorname{tr}(AB) \le \sum_i a_i b_i$

Let $A, B$ be $n \times n$ Hermitian matrices over an RCLike field. Write $a_1 \ge a_2 \ge \dots$ and $b_1 \ge b_2 \ge \dots$ for their eigenvalues sorted in decreasing order — in Lean these are Mathlib's eigenvalues₀, indexed by Fin (Fintype.card n) and antitone in the index.

Statement.

i.e. the trace pairing of two Hermitian matrices is maximized by pairing eigenvalues in matching order.

This is the Hermitian case of von Neumann's trace inequality. The formalized proof combines the eigenbasis identity RHLinalg.re_trace_mul_eq_eigenvalue_bilinear ($\operatorname{Re}\operatorname{tr}(AB)$ as an eigenvalue bilinear form weighted by $\|W_{kl}\|^2$ for a unitary $W$), the fact that this weight matrix is doubly stochastic (RHLinalg.normSqMatrix_mem_doublyStochastic_of_unitary), and the Birkhoff–rearrangement bound RHLinalg.bilinear_doublyStochastic_le_of_monovary.

In the module Zeta23.LinAlg.VonNeumann it is consumed by the rank–trace inequality RHLinalg.rank_trace_ineq, the key matrix-variational estimate feeding the assembly of Theorem A.