The spectral Mazur distance squared as an overlap-weighted sum of scalar Mazur terms

Fix a finite-dimensional complex inner-product space $E$ and a real number $p$ (no hypothesis is placed on $p$). Let $(e_i)_{i\in\iota}$ and $(f_j)_{j\in\kappa}$ be orthonormal bases of $E$ indexed by finite index types $\iota,\kappa$, with real numbers $a:\iota\to\mathbb R$, $b:\kappa\to\mathbb R$ attached to them. Write $\mathrm{diag}_e(c)$ for the self-adjoint operator on $E$ with $\mathrm{diag}_e(c)\,e_i=c_i\,e_i$ (spectralDiagonal), and for $h:\mathbb R\to\mathbb R$ write $h(c)$ for the tuple $i\mapsto h(c_i)$.

Let $\psi_p(x) = \operatorname{sign}(x)\,|x|^{p/2}$ for $x\ne0$, with $\psi_p(0)=0$, be the scalar Mazur map (scalarMazur). The spectral Mazur distance squared of $(e,a)$ against $(f,b)$ is

This is the real-valued definition spectralMazurDistanceSq. With $\operatorname{ov}(e_i,f_j)=|\langle e_i,f_j\rangle|^2$ the squared overlap of two basis vectors (orthonormalBasisOverlap), the theorem states

This is the second of two exact finite double-sum decompositions (the other is for the trace-level Bregman divergence) that let a scalar comparison known for every pair of real numbers be lifted, with the overlap weights $\operatorname{ov}(e_i,f_j)$ — nonnegative and summing to $1$ along every row and column — unchanged in its constants, to a comparison between traces of finite-dimensional Hermitian operators.

Formalization Note The identity holds for every real $p$ and needs no hypothesis on it: both sides are already expressed through the fully totalized real power $\psi_p$, and the right-hand side is manifestly a sum of squares whatever the sign or size of $p$.