Mission
Sharp diagonal Hlawka constant: cutoff 32
Log in to contributeGoal
Extend the sharp diagonal Hlawka formula to smaller exponents.
The foundation mission establishes the least uniform complex coordinate Hlawka constant for every real exponent p ≥ 256. This entry proposes the cutoff 32: the same cyclic constant must be optimal for every real exponent at or above the proposed cutoff, across all finite complex coordinate dimensions and arbitrary triples, including unequal norms.
Use the foundation's unchanged definitions of the coordinate norm, Hlawka constant, and cyclic constant. The goal combines admissibility and uniform optimality in a single IsLeast statement.
Foundation: https://prove2.me/missions/Sharp_diagonal_Hlawka_constants%3A_foundation_and_proved_cutoff_256
theorem HlawkaSchatten.DiagonalConstruction.campaign_cutoff32 :
∀ p : ℝ, 32 ≤ p →
IsLeast {C : ℝ | ∀ n : ℕ,
HasHlawkaConstant (lpNorm p : (Fin n → ℂ) → ℝ) C}
(cyclicConstant p) := by sorryFor every real exponent p ≥ 32, 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 open leaves. Every sub-goal is proved or awaiting decomposition.