Trace positivity: $\operatorname{Re}\operatorname{tr}(AB) \ge 0$ for positive semidefinite $A, B$

Let $A, B$ be $n \times n$ matrices over an RCLike field, both positive semidefinite.

Statement.

The proof diagonalizes $A = U D U^{\mathsf H}$: then $\operatorname{tr}(AB) = \operatorname{tr}\bigl((U^{\mathsf H} B U) D\bigr) = \sum_i \lambda_i \, (U^{\mathsf H} B U)_{ii}$, where each eigenvalue $\lambda_i \ge 0$ (PSD spectrum) and each diagonal entry $(U^{\mathsf H} B U)_{ii} \ge 0$ (diagonal of a positive semidefinite matrix).

In the module Zeta23.LinAlg.RankTrace this standard fact is consumed by the rank–trace inequality RHLinalg.rank_trace_ineq, where cross terms of the form $\operatorname{tr}(P\,Q_\pm)$ between a positive semidefinite matrix and the positive/negative parts of a Hermitian matrix must be discarded with the correct sign.