Mission

Sharp diagonal Hlawka constants: lower the cutoff to 50Open 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\ge62$ , also holds for every real $p\ge50$ . This is an open problem: no proof is known, and the technique that reached 62 cannot go further. 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-62 mission already covers every $p\ge62$ , the new work is the range from 50 to 62.

The cutoff came down from 256 to 62 across nine missions. The step from 90 to 80 used a weighted pair-curvature and confinement estimate introduced by moona3k, and further refinement pushed it from 80 through 70 to 62. The confinement method is now exhausted: at $p=61$ , every confinement radius whose tangent model stays positive already makes the budget-7 box factor larger than 1. Reaching 50 requires a fundamentally new idea. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 50 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
Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

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

PROVED

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

For every real exponent p ≥ 50, 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 50 ≤ p < 62; the accepted cutoff-62 theorem covers every p ≥ 62. The confinement method used through cutoff 62 cannot reach this range.

Frontier · Open leaf nodes

Recent activity