A linear lower bound $\tfrac{939}{2000}p<K_p$ for the cyclic candidate constant

Proved

HlawkaSchatten.DiagonalConstruction.cyclicConstant_gt_separator

by savarin · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

hlawka-schattenscalar-estimatesharp-constanttail-bound

For a real exponent $p$ and $t\ge0$ , let $A_p(t)=(t^p+2)^{1/p}$ , $B_p(t)=(2|1-t|^p+2^p)^{1/p}$ ; let

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

be the cyclic ratio, and let

K_p \;=\; \sup\{\,R_p(t) : 1/2\le t\le2\,\}

be the cyclic candidate constant.

The theorem states that for every real $p\ge256$ ,

\frac{939}{2000}\,p \;<\; K_p.

It shows that $K_p$ grows at least linearly in $p$ , with an explicit rational slope. Elsewhere in the diagonal construction, after a hypothetical failure of the $K_p$ -Hlawka inequality has been relabeled so its total norm is the largest of the four vectors involved and rescaled so its three singleton norms sum to one, this lower bound on $K_p$ is compared against a matching upper bound (from a separate scalar-envelope estimate) at the reference value $53/150$ ; that comparison is what confines such a rescaled failure's total norm below $53/150$ .

Formalization Note. The proof evaluates $R_p$ at the parameter constructionParameter p := Real.exp (-(Real.log p * p⁻¹)), i.e. $t^*=\exp(-\log(p)/p)=p^{-1/p}$ for $p>0$ ; for $p\ge256$ it satisfies $1/2\le t^*\le1$ , so in particular $t^*\ge0$ , and for $t\ge0$ the quantities $A_p(t)$ and $B_p(t)$ are the coordinate $p$ -norms of each of the cyclic vectors $(-t,1,1),(1,-t,1),(1,1,-t)\in\mathbb R^3$ and of each of their pairwise sums.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Convex.Deriv
import Mathlib.Analysis.Convex.Function
import Mathlib.Analysis.Convex.Jensen
import Mathlib.Analysis.Convex.SpecificFunctions.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.NormPow
import Mathlib.Analysis.Normed.Lp.PiLp
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Real.Basic
import Mathlib.Data.Sign.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Topology.Instances.Sign
import Mathlib.Topology.Order.Compact

/-
Copyright (c) 2026 Ezzeri Esa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ezzeri Esa
-/

/-!
# Explicit uniform estimates above the cutoff

Rational logarithm bounds separate the cyclic witness and scalar envelope
at the common intermediate value `939 * p / 2000`.
-/

open HlawkaSchatten.DiagonalConstruction

Formal statement

theorem HlawkaSchatten.DiagonalConstruction.cyclicConstant_gt_separator {p : ℝ} (hp : 256 ≤ p) :
    (939 / 2000 : ℝ) * p < cyclicConstant p := by sorry

Source

https://github.com/savarin/hlawka-schatten/blob/79aa498bfcf7b22bd91d771fb32ec278e2d4704b/HlawkaSchatten/DiagonalConstruction/TailEstimates.lean#L153-L169

Human review

Endorsed by Shuze Chen · Sep 29, 2026
Confirmed by the moderator at approval.
Endorsed by savarin · Sep 29, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by marwahaha · Sep 30, 2026

View graph

A linear lower bound 9392000p<Kp\tfrac{939}{2000}p<K_p2000939​p<Kp​ for the cyclic candidate constant

A linear lower bound $\tfrac{939}{2000}p<K_p$ for the cyclic candidate constant