Prove2Me

Residual-budget localization of a Hlawka counterexample on [32,50][32,50]

Proved
HlawkaSchatten.DiagonalCutoff32.contract32

by @bwdaugherty · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysis

Let 32≤p≤5032\le p\le 50 and let XX be a real 3×33\times 3 matrix with entries in the coarse box (D=[−1.158,−0.555]D=[-1.158,-0.555] for diagonal entries and O=[0.79,1.158]O=[0.79,1.158] for off-diagonal entries), row norms summing to 33, ∥X0+X1+X2∥p<3q(p)\|X_0+X_1+X_2\|_p<3q(p) for the slab envelope radius q(p)q(p), and pair-gap sum below 2/(0.448 p)2/(0.448\,p). Then

−1.065≤Xii≤−0.625,0.849≤Xji≤1.121(j≠i).-1.065\le X_{ii}\le -0.625,\qquad 0.849\le X_{ji}\le 1.121\quad (j\ne i).

The proof contracts the coarse box by a residual-budget argument with a finite-pp two-coordinate cost, certified uniformly on sub-slabs of exponents.

Preamble
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Basic
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Localization
import Definitions.Def_HlawkaSchatten_GapComparison
import Definitions.Def_HlawkaSchatten_DiagonalCutoff32_SlabRadius
import Mathlib

open HlawkaSchatten HlawkaSchatten.DiagonalConstruction
open HlawkaSchatten.DiagonalCutoff32
Formal statement
theorem HlawkaSchatten.DiagonalCutoff32.contract32 : ∀ p : ℝ, 32 ≤ p → p ≤ 50 → ∀ X : Triple,
    (∀ j i : Fin 3, if j = i then -(1158/1000 : ℝ) ≤ X j i ∧ X j i ≤ -(555/1000 : ℝ)
      else (79/100 : ℝ) ≤ X j i ∧ X j i ≤ (1158/1000 : ℝ)) →
    lpNorm p (X 0) + lpNorm p (X 1) + lpNorm p (X 2) = 3 →
    lpNorm p (X 0 + X 1 + X 2) < 3 * slabRadius p →
    pairGapSum (lpNorm p) (X 0) (X 1) (X 2) < 2 / ((448/1000) * p) →
    ∀ j i : Fin 3, if j = i then -(1065/1000 : ℝ) ≤ X j i ∧ X j i ≤ -(625/1000 : ℝ)
      else (849/1000 : ℝ) ≤ X j i ∧ X j i ≤ (1121/1000 : ℝ) := by sorry
Source
Sharp diagonal Hlawka constant campaign, cutoff-32 entry (https://prove2.me/campaigns/sharp-diagonal-hlawka-constant); definitions of the foundation mission (Ezzeri Esa, Apache-2.0).

View graph