Mission

Sharp diagonal Hlawka constants: lower the cutoff to 16Open Problem

Functional Analysis·Captain: savarin

The 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. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge32$ , also holds for every real $p\ge16$ . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-32 mission already covers every $p\ge32$ , the new work is the range from 16 to 32.

The cutoff came down from 256 to 32 across eleven missions. The first phase (256 to 62) used a confinement estimate, exhausted at $p=61$ . The second phase (62 to 32) used a new technique that broke through the confinement barrier. Whether it extends to 16 is not known; 16 asks for sixteen more units below the current best.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. The campaign conjectures the formula for all $p\ge2$ . Any proof for a cutoff of 16 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library

Established results on Prove2Me

Goal · The least uniform complex coordinate Hlawka constant for p ≥ 16

PROVED

theorem HlawkaSchatten.DiagonalCutoff.cutoff16 :
    ∀ p : ℝ, 16 ≤ p →
      IsLeast {C : ℝ | ∀ n : ℕ,
        HasHlawkaConstant (lpNorm p : (Fin n → ℂ) → ℝ) C}
        (cyclicConstant p) := by sorry

For every real exponent p ≥ 16, let N_p(x) be the foundation's finite coordinate p-norm and let K_p be its unchanged cyclicConstant p, defined as the supremum of the cyclic ratio over t ∈ [1/2, 2].

Then K_p is the least real constant C such that the triple deficit N_p(x) + N_p(y) + N_p(z) − N_p(x + y + z) is at most C times the pair-deficit sum 2(N_p(x) + N_p(y) + N_p(z)) − N_p(x + y) − N_p(x + z) − N_p(y + z), for every natural-number dimension n and all complex vectors x, y, z in that dimension.

This combines admissibility and optimality uniformly over all finite complex coordinate dimensions. It includes dimension zero and arbitrary triples with unequal or zero norms. The same shared definitions are used throughout; the claim concerns complex diagonal matrices via their coordinate norms.

No proof is known for 16 ≤ p < 32; the accepted cutoff-32 theorem covers every p ≥ 32. Both the original confinement method (exhausted at 62) and the technique that reached 32 are available as prior art.

Frontier · Open leaf nodes

Recent activity