Papers With

← All papers
First page of Upper bounds for Jung constants of $\ell_1^d$

Upper bounds for Jung constants of $\ell_1^d$

Xiao Li

math.MG Oct 6, 2026 · v1 math.CO
formalization geometry combinatorics
Read PDF arXiv abstract Code
TL;DR
The general upper bound on Jung constants of ℓ_1^{4k+1} and the five-dimensional sharpness result are formalized in Lean, with an axiom audit, in a public repository.
Abstract
For every integer $k\ge1$, we prove that each nonempty bounded set in real $\ell_1^{4k+1}$ has an ambient enclosing ball of radius at most $(4k-1)/(4k)$ times its diameter. The bound is sharp in dimension five: $J(\ell_1^5)=3/4$. If a Hadamard matrix of order $4k$ exists, then $J(\ell_1^{4k-1})=J(\ell_1^{4k})=J(\ell_1^{4k+1})=(4k-1)/(4k)$. The upper bound for every $k\ge1$ has been formalized in Lean.
Problem

The Jung constant J(ℓ_1^d) is the worst-case ratio of the minimal enclosing-ball radius to the diameter of bounded sets in ℓ_1^d. The exact value of J(ℓ_1^5) was listed as unknown in a 2019 survey, and Ivanov's conjecture predicts values tied to Hadamard matrices.

Approach

A contact reduction yields balanced configurations of contact points. Coordinate-gap identities then convert these into weighted cut semimetrics, which reduces the radius bound to a cut inequality. For k≥2 a quadratic-form estimate bounds the cut capacity, and a six-label capacity estimate handles dimension five. Both results are machine-checked in Lean, and an audit confirms that 151 declarations use only the standard axioms.

Results

Every bounded set in ℓ_1^{4k+1} has an enclosing ball of radius at most (4k−1)/(4k) times its diameter, and J(ℓ_1^5)=3/4. Whenever a Hadamard matrix of order 4k exists, J(ℓ_1^{4k−1})=J(ℓ_1^{4k})=J(ℓ_1^{4k+1})=(4k−1)/(4k), which settles Ivanov's conjecture in dimension h+1.