The least uniform complex coordinate Hlawka constant for p ≥ 21

Proved

HlawkaSchatten.DiagonalConstruction.campaign_cutoff21

by Yuxuan Xu · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisdiagonal-constructionhlawka-schattenoptimal-constant

For every real exponent p ≥ 21, 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.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Basic
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Definitions.Def_HlawkaSchatten_GapComparison
import Mathlib.Analysis.Complex.Circle
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.Convex.Function
import Mathlib.Analysis.Convex.Integral
import Mathlib.Analysis.Convex.Jensen
import Mathlib.Analysis.Convex.SpecificFunctions.Basic
import Mathlib.Analysis.Convex.SpecificFunctions.Pow
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.NormPow
import Mathlib.Analysis.Normed.Lp.PiLp
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Real.Basic
import Mathlib.Data.Sign.Basic
import Mathlib.LinearAlgebra.Dimension.Finite
import Mathlib.MeasureTheory.Group.Integral
import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Mathlib.MeasureTheory.Measure.Haar.Basic
import Mathlib.Tactic.Abel
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Module
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Mathlib.Topology.Instances.Sign
import Mathlib.Topology.Order.Compact

/-! # The least dimension-independent complex coordinate Hlawka constant

This packages admissibility and the three-coordinate cyclic obstruction into
one statement, with an explicit lower cutoff on the real exponent.
-/

open HlawkaSchatten
open HlawkaSchatten.DiagonalConstruction

Formal statement

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

Source

Yuxuan Xu (徐宇轩), School of Computer Science, Wuhan University. A computer-assisted sharp diagonal Hlawka inequality for real exponents p >= 21, v1, 17 October 2026. https://github.com/Anchen-AI4Math/hlawka-diagonal-certificates/blob/2f1ec21c8ce4e3d9de33f57119f73f8504de0bd3/paper/main.pdf . LaTeX: https://github.com/Anchen-AI4Math/hlawka-diagonal-certificates/blob/2f1ec21c8ce4e3d9de33f57119f73f8504de0bd3/paper/main.tex . Reproducibility: https://github.com/Anchen-AI4Math/hlawka-diagonal-certificates/blob/2f1ec21c8ce4e3d9de33f57119f73f8504de0bd3/results/release-replay.json . AI-assisted research preprint; independent analytic review pending; no new Lean proof. Main Theorem 1.1. The campaign template is preserved, changing only its declaration name and numeric cutoff.

Read-back

What the Lean code literally says, in plain math · GPT-6 (Codex independent sub-agent)

For every real number $p\ge 21$ , let $N_{p,n}(x)=\bigl(\sum_{i=0}^{n-1}|x_i|^p\bigr)^{1/p}$ for each natural number $n$ and each vector $x\in\mathbb C^n$ , where $|x_i|$ is the complex modulus, and define $A_p(t)=(t^p+2)^{1/p}$ , $B_p(t)=(2|1-t|^p+2^p)^{1/p}$ , and $K_p=\sup\bigl\{\frac{3A_p(t)-3^{1/p}|2-t|}{6A_p(t)-3B_p(t)}:t\in[\tfrac12,2]\bigr\}$ . Then $K_p$ is the least real number $C$ such that, for every natural number $n$ and all $x,y,z\in\mathbb C^n$ , $N_{p,n}(x)+N_{p,n}(y)+N_{p,n}(z)-N_{p,n}(x+y+z)\le C\bigl[(N_{p,n}(x)+N_{p,n}(y)-N_{p,n}(x+y))+(N_{p,n}(x)+N_{p,n}(z)-N_{p,n}(x+z))+(N_{p,n}(y)+N_{p,n}(z)-N_{p,n}(y+z))\bigr]$ . Explicitly, this inequality holds with $C=K_p$ simultaneously for every such dimension and triple, and $K_p\le C$ for every real $C$ for which it holds simultaneously for every dimension and triple; the competing constants $C$ have no separately imposed sign restriction. The quantifiers include zero vectors and $n=0$ : in dimension zero the coordinate sum is empty, $N_{p,0}=0$ , and the required inequality is $0\le 0$ for every real $C$ .

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by Yuxuan Xu · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph