The real coordinate Hlawka bound for $p \ge 62$

Proved

HlawkaSchatten.DiagonalCutoff.real_bound62

by moona3k · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

hlawka-schattensharp-constant

For every real exponent $p\ge 62$ and every finite dimension, the cyclic constant is a Hlawka comparison constant for the real coordinate $p$ -norm.

The accepted real bound covers every $p\ge 63$ . This statement extends that bound down to $p=62$ , including unequal or zero vectors and dimension zero.

Formalization Note. The claim is HasHlawkaConstant for lpNorm p on Fin n → ℝ, with constant cyclicConstant p.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Basic
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Definitions.Def_HlawkaSchatten_GapComparison

open HlawkaSchatten HlawkaSchatten.DiagonalConstruction

Formal statement

theorem HlawkaSchatten.DiagonalCutoff.real_bound62 :
    ∀ p : ℝ, 62 ≤ p → ∀ n : ℕ,
      HasHlawkaConstant (lpNorm p : (Fin n → ℝ) → ℝ)
        (cyclicConstant p) := by sorry

Source

https://prove2.me/campaigns/sharp-diagonal-hlawka-constant

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by moona3k · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by savarin · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The real coordinate Hlawka bound for p≥62p \ge 62p≥62

The real coordinate Hlawka bound for $p \ge 62$