The least uniform complex coordinate Hlawka constant for p ≥ 50

Proved

HlawkaSchatten.DiagonalCutoff.cutoff50

by savarin · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisdiagonal-constructionhlawka-schattenoptimal-constant

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.

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.DiagonalCutoff.cutoff50 :
    ∀ p : ℝ, 50 ≤ p →
      IsLeast {C : ℝ | ∀ n : ℕ,
        HasHlawkaConstant (lpNorm p : (Fin n → ℂ) → ℝ) C}
        (cyclicConstant p) := by sorry

Source

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

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

For every real number $p$ with $p \ge 50$ (any real, not necessarily an integer; nothing is asserted for $p < 50$ ), the number $c_p$ defined below is the least element of the set $S_p$ defined below.

Norm. Take $n \in \mathbb{N}$ and $x = (x_1, \dots, x_n) \in \mathbb{C}^n$ . The entries are complex, and vectors are added coordinatewise. Set

\|x\|_p = \Big(\sum_{i=1}^{n} |x_i|^p\Big)^{1/p},

where $|x_i|$ is the usual complex modulus.

Admissible constants. $S_p$ is the set of all real numbers $C$ , with no sign restriction, such that the inequality below holds for every $n \in \mathbb{N}$ , including $n = 0$ , and for all $x, y, z \in \mathbb{C}^n$ , with no further restriction:

\|x\|_p + \|y\|_p + \|z\|_p - \|x+y+z\|_p \;\le\; C\Big[\big(\|x\|_p + \|y\|_p - \|x+y\|_p\big) + \big(\|x\|_p + \|z\|_p - \|x+z\|_p\big) + \big(\|y\|_p + \|z\|_p - \|y+z\|_p\big)\Big]

The bracket equals $2(\|x\|_p + \|y\|_p + \|z\|_p) - \|x+y\|_p - \|x+z\|_p - \|y+z\|_p$ . A single $C$ must work in all dimensions at once.

For $n = 0$ , the only vector is the empty tuple, whose norm is $0$ . The condition then reads $0 \le 0$ and constrains nothing.
For $n = 1$ , $\|x\|_p = |x_1|$ .

The constant. For $\tfrac12 \le t \le 2$ let

A_p(t) = (t^p + 2)^{1/p}, \qquad B_p(t) = \big(2\,|1-t|^p + 2^p\big)^{1/p}, \qquad R_p(t) = \frac{3A_p(t) - 3^{1/p}\,|2-t|}{6A_p(t) - 3B_p(t)},

c_p = \sup\big\{R_p(t) : \tfrac12 \le t \le 2\big\}.

The formula for $c_p$ does not involve $n$ . Every power here and in the norm is a real power of a nonnegative number with a positive exponent, so each has its usual meaning.

On this interval the denominator of $R_p$ is strictly positive. It is positive exactly when $2^p(t^p+1) > 2|1-t|^p$ . The left side exceeds $2^{50}$ , and the right side is at most $2$ because $|1-t| \le 1$ there. So the formal convention $a/0 = 0$ never applies.

$R_p$ is also continuous on the interval. Its values therefore form a nonempty bounded set, and $c_p$ is their ordinary supremum, which is attained. The formal convention that an empty or unbounded set of reals has supremum $0$ does not apply either.

Claim. "Least element" means both of the following:

$c_p \in S_p$ : for every $n$ and all $x, y, z \in \mathbb{C}^n$ , the displayed inequality holds with $C = c_p$ .
$c_p \le C$ for every $C \in S_p$ : equivalently, for each real $C < c_p$ there exist some $n$ and some $x, y, z \in \mathbb{C}^n$ for which the inequality fails. The dimension may depend on $C$ , and no particular dimension is named.

Human review

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

View graph