The sphere-packing constant equals the lattice-packing constant in every dimension

The theorem asserts: for every natural number $r\in\{0,1,2,3,\dots\}$,

an equality of two elements of the extended non-negative reals $[0,\infty]$. There are no hypotheses on $r$ whatsoever; in particular $r=0$ and $r=1$ are included. The theorem is stated without a proof in this file. The two sides are the non-Mathlib quantities defined as follows.

Throughout, $\mathbb{R}^r$ is the Euclidean space of real $r$-tuples with the Euclidean ($\ell^2$) distance $\operatorname{dist}$; for $r=0$ it is the single point $0$. $\operatorname{vol}$ is the default volume on this finite-dimensional real inner-product space: the Haar measure normalised so that the parallelepiped spanned by an orthonormal basis has measure $1$ (standard Lebesgue measure; in dimension $0$ the one-point space has mass $1$), with values in $[0,\infty]$. $B(x,\rho)=\{y:\operatorname{dist}(y,x)<\rho\}$ is the open ball.

• A subset $C\subseteq\mathbb{R}^r$ (arbitrary: no measurability, discreteness or finiteness assumed) is a unit packing iff

(non-strict inequality). The empty set and all singletons are unit packings.

• The upper density of a subset $C\subseteq\mathbb{R}^r$ is

with $R$ ranging over all reals, division in $[0,\infty]$ ($0^{-1}=\infty$, $\infty^{-1}=0$, so $a/0=\infty$ for $a\neq0$, $0/0=0$, $a/\infty=0$), and the limsup being the infimum of all $a\in[0,\infty]$ such that the ratio is $\le a$ for all sufficiently large $R$ (equivalently $\inf_{R_0\in\mathbb{R}}\sup_{R\ge R_0}$). For $R\le0$ the ball $B(0,R)$ is empty and the ratio is $0/0=0$, which does not affect the limsup. For $r\ge1$ and $R>0$ the ratio lies in $[0,1]$, so $\overline{\delta}(C)\in[0,1]$; $\overline{\delta}(\emptyset)=0$.

• $\Delta_r=\sup\{\overline{\delta}(C): C\subseteq\mathbb{R}^r \text{ a unit packing}\}$, the supremum in $[0,\infty]$ over all unit packings (formally an indexed supremum over all subsets $C$ and all proofs that $C$ is a unit packing, non-unit-packings contributing $0$). The index set is non-empty because $\emptyset$ is a unit packing. No discreteness, countability or measurability of $C$ is required.
• $\Delta^{L}_r=\sup\{\overline{\delta}(L): L \text{ an additive subgroup of } \mathbb{R}^r,\ L \text{ a unit packing},\ \operatorname{span}_{\mathbb{R}}(L)=\mathbb{R}^r\}$, where $L$ ranges over all additive subgroups of $\mathbb{R}^r$ (subsets containing $0$, closed under $+$ and negation; no discreteness, closedness, finite generation or $\mathbb{Z}$-basis is assumed), "unit packing" and $\overline{\delta}$ refer to the underlying set of $L$, and $\operatorname{span}_{\mathbb{R}}(L)$ is the smallest real linear subspace containing the set $L$, required to be all of $\mathbb{R}^r$. Formally the supremum is over $L$ and over proofs of the two side conditions, failed conditions contributing $0$; it equals $0$ if no subgroup satisfies both.

So the claim is: for every $r\ge0$, the supremum of upper densities over all unit packings of $\mathbb{R}^r$ equals the supremum of upper densities over those additive subgroups of $\mathbb{R}^r$ that are unit packings and linearly span $\mathbb{R}^r$ (both suprema in $[0,\infty]$; the assertion is an equality, i.e. both $\Delta_r\le\Delta^L_r$ and $\Delta^L_r\le\Delta_r$). Edge case $r=0$: $\mathbb{R}^0=\{0\}$, $B(0,R)=\{0\}$ for $R>0$ with $\operatorname{vol}(\{0\})=1$; the unit packings are $\emptyset$ (density $0$) and $\{0\}$ (density $1$), so $\Delta_0=1$; the only additive subgroup is $\{0\}$, which is a unit packing spanning the trivial space, so $\Delta^L_0=1$ and the $r=0$ instance reads $1=1$.