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

Technical Summary: Upper Bounds for Jung Constants of $\ell^d_1$

Problem Statement
The paper addresses the determination of the Jung constant $J(\ell^d_1)$ for the $d$-dimensional real space equipped with the $\ell_1$ norm (Manhattan distance). For a nonempty bounded set $A \subset \mathbb{R}^d$, the Jung constant is defined as the supremum of the ratio between the Chebyshev radius ($rad\, A$) and the diameter ($diam\, A$) over all such sets. Specifically, the author seeks to establish tight upper bounds for $J(\ell^d_1)$ when the dimension $d$ takes the form $4k+1$ for integers $k \ge 1$.

Prior to this work, while classical bounds existed (e.g., $J(\ell^d_1) \le d/(d+1)$ and $J(\ell^{2m}_1) \le (2m-1)/(2m)$), the exact value for dimension $d=5$ (where $k=1$) was listed as unknown in a 2019 survey by Alimov and Tsar'kov. Furthermore, Ivanov's conjecture posited that if a Hadamard matrix of order $h=4k$ exists, then $J(\ell^h_1) = J(\ell^{h+1}_1) = J(\ell^{h+2}_1) = (h-1)/h$.

Methodology
The proof strategy combines geometric reduction techniques with combinatorial estimates on cut metrics:

1. Contact Reduction and Dimension Bounds:
   The author utilizes Lemma 2.1 to reduce the problem to a finite set of "contact points" $y_i$ and associated signs $\sigma_i$ that define the minimal enclosing ball. If the radius $R$ exceeds a specific threshold, Lemma 2.2 establishes that the number of contact points must be exactly $2p$ (where $d=2p-1$) and that the signs must sum to zero. This leads to an inequality involving the sum of distances from an arbitrary point $z$ to these contact points.

2. Quadratic-Form Estimates for Cuts:
   The core technical innovation lies in translating the geometric distance constraints into a problem about weighted sums of cut semimetrics.

   • General Case ($k \ge 2$): For dimensions $d = 4k+1$ (where $p = 2k+1 \ge 5$), the author employs Lemma 3.1. This lemma provides an upper bound $B_p$ for the weighted sum of cut sizes ($\Phi$) given constraints on pairwise distances and the number of "balanced" cuts. The proof of Lemma 3.1 relies on a quadratic-form analysis involving a matrix of distances and specific vector constructions to derive the bound.
   • Five-Dimensional Case ($k=1$): The general quadratic-form bound is insufficient for $p=3$ (dimension 5). Section 5 introduces a specialized "six-label capacity estimate" (Proposition 5.1). This involves a combinatorial analysis of cuts on a set of six labels, classifying balanced cuts by their graph representations (edges of $K_5$) and constructing explicit weight certificates to prove the bound $\Phi \le 9/2$.

3. Coordinate Gaps and Arbitrary Sets:
   Lemma 4.1 bridges the gap between finite contact sets and arbitrary bounded sets by utilizing coordinate-wise medians to construct cut metrics that preserve pairwise distances. Lemma 4.2 extends the finite results to arbitrary nonempty bounded sets via a compactness argument.

4. Sharpness and Hadamard Matrices:
   To prove the bounds are sharp, the paper constructs specific point sets. For the lower bound, it utilizes properties of Hadamard matrices (Proposition 7.1). For the specific case of $d=5$, a four-point set is explicitly constructed to demonstrate that the radius cannot be smaller than $3/4$ of the diameter.

Key Contributions and Results

• Main Theorem (Theorem 1.1): For every integer $k \ge 1$, the Jung constant for dimension $4k+1$ satisfies the unconditional upper bound:
  $$J(\ell^{4k+1}_1) \le \frac{4k-1}{4k}$$
  This establishes that every nonempty bounded set in $\mathbb{R}^{4k+1}$ has an ambient enclosing ball of radius at most $\frac{4k-1}{4k}$ times its diameter.

• Resolution of the Five-Dimensional Case: The paper proves that $J(\ell^5_1) = 3/4$. This resolves the open question noted in the Alimov and Tsar'kov survey by establishing both the upper bound and a matching lower bound for this specific dimension.

• Confirmation of Ivanov's Conjecture (Conditional): Corollary 1.2 states that if a Hadamard matrix of order $4k$ exists, then the exact value is determined for three consecutive dimensions:
  $$J(\ell^{4k-1}_1) = J(\ell^{4k}_1) = J(\ell^{4k+1}_1) = \frac{4k-1}{4k}$$
  This confirms the conjectured value for the dimension $h+1$ (where $h=4k$) and unifies the values for dimensions $h-1, h,$ and $h+1$ under the existence of Hadamard matrices. Without this assumption, the paper provides the upper bound for $4k+1$ and the lower bound via Hadamard examples, but does not claim the exact value for all $4k+1$ dimensions unconditionally.

• Formalization: The upper bound for every $k \ge 1$ and the sharpness result for dimension 5 have been formally verified using the Lean theorem prover. The code is available in a public repository, with dependencies restricted to standard classical axioms.

Significance and Claims
The paper claims to provide a tight upper bound for the Jung constant in dimensions of the form $4k+1$ unconditionally, and the exact value for these dimensions (as well as $4k-1$ and $4k$) under the assumption of the existence of Hadamard matrices. It specifically settles the long-standing open case for dimension 5. The work refines the understanding of how the geometry of $\ell_1$ spaces behaves in high dimensions, particularly regarding the relationship between diameter and enclosing radius.

The author notes that the bound derived in Lemma 3.1 is specific to the "contact configuration" forced by a radius exceeding the threshold and is not an unconditional upper bound for the Jung constant itself. The significance of the result is framed within the context of classical metric geometry problems, specifically the interplay between combinatorial structures (Hadamard matrices, cut metrics) and geometric constants. The formalization in Lean is highlighted as a verification of the rigorous correctness of the complex combinatorial estimates involved.