Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$. We conjecture that the same formula holds for all $p\ge2$.

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$?

References:

• Wolfram MathWorld, Hlawka's Inequality.
• Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
• Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
• Analytic argument for $p\ge90$, awaiting formalization in Lean.