The cyclic Hlawka bound for self-adjoint operators when p ≥ 256

Let $H$ be a finite-dimensional complex inner-product space, of any dimension. A complex-linear map $A:H\to H$ is self-adjoint if $\langle Ax,y\rangle=\langle x,Ay\rangle$ for all $x,y\in H$; in an orthonormal basis it is a Hermitian matrix. For real $p>1$ its Schatten norm is

where $s_i(A)$ are the singular values of $A$; for self-adjoint $A$ they are the absolute values of its eigenvalues. This is the existing schattenPNorm definition, with no normalization by dimension.

For self-adjoint $A,B,C:H\to H$, the triple deficit and the pair-deficit sum are

and the cyclic constant is the existing DiagonalConstruction.cyclicConstant,

Statement. For every real $p\ge256$, every finite-dimensional complex inner-product space $H$ and all self-adjoint $A,B,C:H\to H$,

This is the self-adjoint case of the general-matrix conjecture HlawkaSchatten.SchattenSharpness.cyclic_bound256, and it is equivalent to it. In one direction it is the special case $E=F=H$ restricted to self-adjoint triples. In the other, the Hermitian dilation $T\mapsto\begin{pmatrix}0&T^*\\T&0\end{pmatrix}$ carries every rectangular operator to a self-adjoint one and multiplies every Schatten norm by the same factor $2^{1/p}$, so a proof of this statement settles the general conjecture.

Formalization Note. Self-adjointness is Mathlib's LinearMap.IsSymmetric. The space $H$ may have any finite dimension, including $0$, $1$ and $2$. No positivity, commutativity, common-eigenbasis or equal-norm hypothesis is imposed.