This mission asks for the final entry of the sharp diagonal Hlawka campaign: the exact Hlawka constant for complex diagonal matrices at every exponent $p\ge2$. The same statement is proved in Lean for every $p\ge4$. Two statements remain open, one on each side of the threshold $p_W=\log 3/\log(3/2)\approx2.7095$.

Hlawka's inequality and its constant

A normed space satisfies Hlawka's inequality if every triple of vectors $x,y,z$ in it satisfies

$$\|x\|+\|y\|+\|z\|+\|x+y+z\|\ \ge\ \|x+y\|+\|y+z\|+\|z+x\|.$$

It holds in every inner product space and in every space that embeds isometrically in $L^1$, including $\ell_p$ for $1\le p\le2$ (Marinescu and Niculescu, §§1–3). It can fail in $\ell_p$: for $x=(-1,1,1)$, $y=(1,-1,1)$, $z=(1,1,-1)$ the left side is $4\cdot3^{1/p}$ and the right side is $6$, so this triple satisfies the inequality exactly when $3^{1/p}\ge\tfrac32$, that is, when $p\le p_W$. Where it fails, one asks for the least factor by which the pair deficits defined below must be multiplied to restore it. Audenaert and Kittaneh ask this for Schatten $p$-norms (§8.2, Problem 7). For diagonal matrices the Schatten norm is the coordinate norm of the diagonal.

• 1942. Hornich states the inequality, with Hlawka's proof for Euclidean space.
• 2012. Audenaert and Kittaneh pose the Schatten-norm question.
• 2024. Marinescu and Niculescu record this failure for every $p>p_W$, and ask in Problem 1 for a proof that $\ell_p(3)$ fails the inequality for every $p>2$.
• Sep 29 – Oct 29, 2026. The exact diagonal formula is proved in Lean for $p\ge256$ (savarin), then $p\ge90$ (BrunoDCDO, formalizing savarin's argument), $p\ge62$ (moona3k), $p\ge32$ (@bwdaugherty), $p\ge21$ (Yuxuan Xu, computer-assisted) and $p\ge4$ (shivm). moona3k also formalizes the failure above $p_W$.
• Oct 2026. Lee proves that the inequality holds in every $\ell_p(n)$ with $2<p\le p_W$ if and only if it holds in $\ell_{p_W}(3)$, and conjectures that it does.

Coordinate norms and the cyclic constant

For a real exponent $p\ge1$ and a vector $x$ with real or complex coordinates, the coordinate norm is $N_p(x)=\big(\sum_i|x_i|^p\big)^{1/p}$ (lpNorm p). For three vectors $x,y,z$ in the same space, the triple deficit and the pair-deficit sum are

$$\Delta_3=N_p(x)+N_p(y)+N_p(z)-N_p(x+y+z),$$ $$\Delta_2=2\big(N_p(x)+N_p(y)+N_p(z)\big)-N_p(x+y)-N_p(x+z)-N_p(y+z).$$

A real number $C$ is a Hlawka constant for $N_p$ when $\Delta_3\le C\,\Delta_2$ for all triples (HasHlawkaConstant). Hlawka's inequality is the case $C=1$.

The cyclic family $(-t,1,1),(1,-t,1),(1,1,-t)$, for $t\in[\tfrac12,2]$, has $\Delta_3/\Delta_2=R_p(t)$, where

$$R_p(t)=\frac{3A_p(t)-3^{1/p}|2-t|}{6A_p(t)-3B_p(t)},\qquad A_p(t)=(t^p+2)^{1/p},\qquad B_p(t)=\big(2|1-t|^p+2^p\big)^{1/p}.$$

The cyclic constant is $K_p=\sup_{t\in[1/2,2]}R_p(t)$ (cyclicConstant p). No constant smaller than $K_p$ works in dimension three. Write

$$p_W=\frac{\log 3}{\log(3/2)}\approx2.7095$$

for the threshold, written $p_0$ on some theorem pages. The triple above is the case $t=1$, and $R_p(1)>1$ exactly when $p>p_W$. Numerically, $K_p=1$ for $2\le p\le p_W$, attained at $t=2$ where $x+y+z=0$, and $K_p$ rises above 1 for $p>p_W$, reaching $K_4\approx1.4671$.

Formalization targets

Goal

For every real $p\ge2$, $K_p$ is the least constant $C$ such that $\Delta_3\le C\,\Delta_2$ for all $x,y,z\in\mathbb C^n$ and every $n$:

$$\forall p\ge2:\qquad K_p=\min\big\{C\in\mathbb R:\ \Delta_3\le C\,\Delta_2\ \text{on }\mathbb C^n\text{ for every }n\big\}.$$

This is campaign_cutoff2, stated with IsLeast. For every $p\ge2$, the cyclic family proves that no smaller constant can work, and the whole statement is proved for every $p\ge4$. What remains is to prove that $K_p$ is a Hlawka constant throughout $2\le p<4$.

The real bound (milestone)

$$\forall p\ge2,\ \forall n,\ \forall x,y,z\in\mathbb R^n:\qquad \Delta_3\le K_p\,\Delta_2.$$

This is real_bound2. The goal follows from it by the proved transfer from real three-dimensional bounds.

The two open statements (milestones)

With the proved range $p\ge4$ and the proved dimension lift, the real bound reduces to the mission's only open leaves:

(A) Hlawka's inequality on $[2,p_W]$, hlawka_holds_below:

$$\forall p\in[2,p_W],\ \forall n,\ \forall x,y,z\in\mathbb R^n:\qquad \Delta_3\le\Delta_2.$$

(B) The sharp bound on $[p_W,4]$ in dimension three, real_three_threshold_to_four:

$$\forall p\in[p_W,4],\ \forall x,y,z\in\mathbb R^3:\qquad \Delta_3\le K_p\,\Delta_2.$$

Together, (A) and (B) imply the real bound, and with it the goal. A proof of Hlawka's inequality in $\ell_{p_W}(3)$ would settle (A), through Lee's two reductions (the second still needs a Lean proof), and would also settle (B) at $p=p_W$, since $K_{p_W}\ge1$. The sharp bound for $p_W<p<4$ would remain.

What a proof would settle

A proof of the goal gives the exact Hlawka constant for complex diagonal matrices, uniformly in the dimension, at every $p\ge2$. That is the campaign's conjecture, and it answers the Audenaert–Kittaneh question for diagonal matrices on that range.

Statement (A) also stands on its own. It would answer Problem 1 of Marinescu and Niculescu in the negative on $(2,p_W]$ and prove Lee's endpoint conjecture (Conjecture 4.9). With the known cases, it would show that for $n\ge3$ the space $\ell_p(n)$ satisfies Hlawka's inequality exactly when $1\le p\le p_W$. By Lee's Theorem 4.5 the same holds for $L_p$ spaces of dimension at least three, none of which embeds isometrically in $L^1$ when $p>2$ (Dor, cited in Marinescu and Niculescu, Remark 2).

Everything from $p\ge256$ down to $p\ge4$ is proved in Lean. Neither (A) nor (B) has a known proof, on paper or in Lean. The evidence for both is numerical: moona3k's searches, posted in the cutoff-89 discussion, and, for (A), Lee's. Of Lee's two reductions, only the dimension reduction is formalized, as real_bound_of_fin_three.

Why the remaining range is hard

Every accepted step from $p\ge256$ to $p\ge4$ uses one argument: suppose a triple beats $K_p$, use a lower bound on $K_p$ to confine it near the cyclic family, and rule it out there. In the later steps the exponent range is cut into short windows.

Whenever one of $x,y,z,x+y+z$ is zero, the deficits satisfy $\Delta_3=\Delta_2$, so Hlawka's inequality, with constant $1$, has whole families of equality cases. At $p=p_W$, the cyclic triple with $t=1$ is another exact equality case. An endpoint proof must remain valid arbitrarily close to these equality families, so an estimate that needs a positive margin $C-1$ does not carry over to $C=1$ without further justification. Numerical evaluations suggest $K_{p_W}=1$; the identity $R_{p_W}(1)=1$ alone does not prove it.

The standard proof for $p\le2$ embeds the space isometrically in $L^1$. For $p>2$, $\ell_p(3)$ has no such embedding (Dor). Writing the norm as a sum of norms of two-dimensional projections would give one, so that route is closed too.

Formalization scope

The environment is Mathlib 0df444a (Lean v4.33.1), with the foundation's unchanged lpNorm, cyclicConstant and HasHlawkaConstant. The goal ranges over Fin n → ℂ for every n : ℕ, including $n=0$, with real $p$ and IsLeast over real constants. No statement assumes normalized, equal-norm or nonzero vectors. (A) is stated over $\mathbb R^n$ for every $n$, but real_bound_of_fin_three lifts any three-dimensional bound with constant at least $\tfrac12$, so $n=3$ suffices. (B) is stated in dimension three. Checking the cyclic family proves only the lower bound, already in Lean, and checks at sampled exponents do not prove interval statements.

Proved results to build on:

• cutoff4: the goal for every $p\ge4$.
• real_bound_of_fin_three: from dimension three to every finite dimension.
• complex_least_of_real_three: from a real three-dimensional bound to the complex goal, with leastness.
• real_three_four_to_six: the real three-dimensional bound on $[4,6]$.
• hlawka_fails_above: failure in $\ell_p(3)$ for every $p>p_W$.

Welcome contributions:

• proofs or reductions of (A) or (B), or of (B) on part of its range, such as $[3,4]$;
• a Lean proof of Lee's Theorem 4.6 (if $\ell_p(3)$ satisfies Hlawka's inequality, so does $\ell_r(3)$ for $1<r<p$), which with the dimension lift reduces (A) to the single space $\ell_{p_W}(3)$;
• Hlawka's inequality at one exponent, such as $p=5/2$, which would already answer Problem 1 in the negative, though it is not on the goal's proof path.

Selected references

• H. Hornich, Eine Ungleichung für Vektorlängen, Mathematische Zeitschrift 48 (1942), 268–274. doi:10.1007/bf01180017
• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint (2012), §8.2, Problem 7. arXiv:1201.5232v3
• D.-Ş. Marinescu and C. P. Niculescu, A survey of the Hornich–Hlawka inequality, arXiv preprint (2024), Problem 1 and Remark 2. arXiv:2407.03278v1
• S. Lee, Constructions and reductions on the Hornich–Hlawka inequality and its generalizations, arXiv preprint (2026), Theorems 1.1, 4.3, 4.5 and 4.6, Conjecture 4.9. arXiv:2610.23785v1
• Yuxuan Xu, A computer-assisted sharp diagonal Hlawka inequality for real exponents p ≥ 21, research preprint (2026). PDF
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository (2026), revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library