The cyclic Hlawka bound for real symmetric operators when p ≥ 256

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

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

For symmetric $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 real inner-product space $H$ and all symmetric $A,B,C:H\to H$,

This is the real symmetric case of HlawkaSchatten.SchattenSharpness.selfAdjoint_cyclic_bound256, and it is equivalent to it: a complex self-adjoint operator, viewed as a real-linear map with inner product $\mathrm{Re}\langle x,y\rangle$, is symmetric with every singular value repeated twice, so $N_p$ is multiplied by $2^{1/p}$; conversely, complexifying a real symmetric operator keeps every singular value with its multiplicity. The self-adjoint statement is itself equivalent to the general-matrix conjecture HlawkaSchatten.SchattenSharpness.cyclic_bound256 through the Hermitian dilation, which carries every rectangular operator to a self-adjoint one and multiplies $N_p$ by $2^{1/p}$. A proof of the present statement therefore proves that conjecture.

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