Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Real three-dimensional Hlawka admissibility on [26, 32]

Proved
HlawkaSchatten.DiagonalCutoff21.real_three_window26

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

convexityhlawka-schattenlp-norm

For each real exponent p in the closed interval [26,32] and all real three-coordinate vectors x,y,z, their triple norm deficit is at most K_p times the sum of their three pair norm deficits. K_p and lpNorm are the unchanged campaign definitions. The conclusion covers all triples, including unequal norms and zero vectors, with no localization, normalization, certificate-validity or convexity assumption.

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

open HlawkaSchatten
open HlawkaSchatten.DiagonalConstruction
Formal statement
theorem HlawkaSchatten.DiagonalCutoff21.real_three_window26 :
    ∀ p : ℝ, 26 ≤ p → p ≤ 32 →
      HasHlawkaConstant (lpNorm p : (Fin 3 → ℝ) → ℝ)
        (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. Section 7, paragraph following equation (40): exclusion of all real three-dimensional counterexamples on Window II. Sections 3-6 and Lemma 8.1 supply the argument.
Read-back

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

For every real number ppp with 26≤p≤3226\le p\le3226≤p≤32, and every three vectors x=(x1,x2,x3)x=(x_1,x_2,x_3)x=(x1​,x2​,x3​), y=(y1,y2,y3)y=(y_1,y_2,y_3)y=(y1​,y2​,y3​), and z=(z1,z2,z3)z=(z_1,z_2,z_3)z=(z1​,z2​,z3​) in R3\mathbb R^3R3, define Np(v)=(∑i=13∣vi∣p)1/pN_p(v)=\left(\sum_{i=1}^{3}|v_i|^p\right)^{1/p}Np​(v)=(∑i=13​∣vi​∣p)1/p for v∈R3v\in\mathbb R^3v∈R3 and let CpC_pCp​ be the real supremum of the set {3(tp+2)1/p−31/p∣2−t∣6(tp+2)1/p−3(2∣1−t∣p+2p)1/p: t∈R, 12≤t≤2}\left\{\dfrac{3(t^p+2)^{1/p}-3^{1/p}|2-t|}{6(t^p+2)^{1/p}-3\left(2|1-t|^p+2^p\right)^{1/p}}:\ t\in\mathbb R,\ \tfrac12\le t\le2\right\}{6(tp+2)1/p−3(2∣1−t∣p+2p)1/p3(tp+2)1/p−31/p∣2−t∣​: t∈R, 21​≤t≤2}, where powers are real powers and the quotient is interpreted using total real division (its value is 000 if its denominator is 000). Then Np(x)+Np(y)+Np(z)−Np(x+y+z)≤Cp((Np(x)+Np(y)−Np(x+y))+(Np(x)+Np(z)−Np(x+z))+(Np(y)+Np(z)−Np(y+z)))N_p(x)+N_p(y)+N_p(z)-N_p(x+y+z)\le C_p\bigl((N_p(x)+N_p(y)-N_p(x+y))+(N_p(x)+N_p(z)-N_p(x+z))+(N_p(y)+N_p(z)-N_p(y+z))\bigr)Np​(x)+Np​(y)+Np​(z)−Np​(x+y+z)≤Cp​((Np​(x)+Np​(y)−Np​(x+y))+(Np​(x)+Np​(z)−Np​(x+z))+(Np​(y)+Np​(z)−Np​(y+z))), with vector sums taken coordinatewise. There are no restrictions on the vectors or on equality of their NpN_pNp​ values: the assertion includes arbitrary unequal norms, cases in which any vector or any displayed vector sum is zero, and the all-zero triple, for which the inequality is 0≤00\le00≤0.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me