Proof. By the packing condition [eq:packing], the only terms on the left-hand side of [eq:poisson] with $\|\mathbf{x}_j - \mathbf{x}_\ell + \mathbf{x}\| < 2$ are the $m$ diagonal terms where $j=\ell$ and $\mathbf{x}=\mathbf{0}$, each contributing $f(\mathbf{0})=1$. Every other displacement has norm $\ge 2$, where $f \le 0$. Therefore, $$\begin{equation} \label{eq:rhsbound} \sum_{j,\ell=1}^m \sum_{\mathbf{x}\in L} f(\mathbf{x}_j-\mathbf{x}_\ell+\mathbf{x}) \leq m. \end{equation}$$

On the Fourier side, all summands are non-negative. Isolating $\mathbf{k}=\mathbf{0}$ gives: $$\begin{equation} \label{eq:lhsbound} \frac{m^2}{\mathop{\mathrm{Vol}}(L)} \leq \frac{1}{\mathop{\mathrm{Vol}}(L)} \sum_{\mathbf{k}\in L^*} S(\mathbf{k})\widehat f(\mathbf{k}). \end{equation}$$ Combining [eq:rhsbound] and [eq:lhsbound] yields $\frac{m^2}{\mathop{\mathrm{Vol}}(L)} \leq m$, whence $\mathop{\mathrm{Vol}}(L)\geq m$.

On the other hand, the density is $\delta(X) = \frac{m}{\mathop{\mathrm{Vol}}(L)} \frac{\pi^{12}}{12!} = \frac{\pi^{12}}{12!}$, which forces $\frac{m}{\mathop{\mathrm{Vol}}(L)}=1$. Therefore, $\mathop{\mathrm{Vol}}(L)=m$ and $\mathop{\mathrm{Vol}}(L^*) = \frac{1}{m}$. ◻

Proof. In Lemma 3, $\frac{m^2}{\mathop{\mathrm{Vol}}(L)} = m$, so equality holds throughout [eq:poisson]. Consequently, every non-zero real displacement must evaluate to a zero of $f$, which by Theorem 2 gives the displacement spectrum. Likewise, every non-zero Fourier contribution must vanish, establishing [eq:dualvanishing]. ◻

Proof. Since $\mathbf{0} \in X$, for any $\bm{\ell}\in L\setminus\{\mathbf{0}\}$, $\bm{\ell} = \mathbf{0} - (-\bm{\ell}) \in X - X$. Corollary 4 implies $\|\bm{\ell}\|^2\in\{4,6,8,\ldots\}\subset2\mathbb Z$. Thus $L$ is an even lattice, so $\langle\bm{\ell}_1,\bm{\ell}_2\rangle = \frac{1}{2}(\|\bm{\ell}_1+\bm{\ell}_2\|^2 - \|\bm{\ell}_1\|^2 - \|\bm{\ell}_2\|^2)\in\mathbb Z$, which gives $L\subseteq L^*$.

Next, fix $j \in \{1, \dots, m\}$ and $\bm{\ell}\in L$. Both $\mathbf{x}_j$ and $\mathbf{x}_j+\bm{\ell}$ belong to $X$. Since $\mathbf{0}\in X$, Corollary 4 implies $\|\mathbf{x}_j\|^2\in2\mathbb Z$ and $\|\mathbf{x}_j+\bm{\ell}\|^2\in2\mathbb Z$. When $\mathbf{x}_j = \mathbf{0}$, $\langle \mathbf{x}_j, \bm{\ell} \rangle = 0 \in \mathbb{Z}$ trivially. When $\mathbf{x}_j \neq \mathbf{0}$ and $\bm{\ell} \neq \mathbf{0}$, polarization yields: $$\begin{equation} 2\langle\mathbf{x}_j,\bm{\ell}\rangle = \|\mathbf{x}_j+\bm{\ell}\|^2 - \|\mathbf{x}_j\|^2 - \|\bm{\ell}\|^2 \in 2\mathbb Z - 2\mathbb Z - 2\mathbb Z = 2\mathbb Z. \end{equation}$$ Dividing by $2$ gives $\langle\mathbf{x}_j,\bm{\ell}\rangle\in\mathbb Z$ for all $\bm{\ell}\in L$. By definition of the reciprocal lattice $L^* \coloneqq \{\mathbf{y} \in \mathbb{R}^{24} : \langle \mathbf{y}, \bm{\ell} \rangle \in \mathbb{Z} \; \forall \bm{\ell} \in L\}$, this establishes that $\mathbf{x}_j\in L^*$ for each $j \in \{1, \dots, m\}$.

Since $L \subseteq L^*$ and every $\mathbf{x}_j \in L^*$, every integer linear combination of these generators lies in $L^*$. Thus $L \subseteq M \subseteq L^*$. ◻

Proof. For any two generators $\mathbf{u}, \mathbf{v} \in X$, both $\|\mathbf{u}\|^2$ and $\|\mathbf{v}\|^2$ are even integers (since $\mathbf{0} \in X$), and $\|\mathbf{u} - \mathbf{v}\|^2 \in 2\mathbb{Z}$ by Corollary 4. Polarization gives: $$\begin{equation} \langle \mathbf{u}, \mathbf{v} \rangle = \frac{1}{2}\left( \|\mathbf{u}\|^2 + \|\mathbf{v}\|^2 - \|\mathbf{u} - \mathbf{v}\|^2 \right) \in \mathbb{Z}. \end{equation}$$ Thus, all entries of the Gram matrix of generators are integers. For any arbitrary element $\mathbf{w} = \sum_{i} a_i \mathbf{u}_i \in M$ with $a_i \in \mathbb{Z}$ and $\mathbf{u}_i \in X$, the squared norm expands as: $$\begin{equation} \|\mathbf{w}\|^2 = \sum_{i} a_i^2 \|\mathbf{u}_i\|^2 + 2 \sum_{i < j} a_i a_j \langle \mathbf{u}_i, \mathbf{u}_j \rangle \in 2\mathbb{Z}. \end{equation}$$ Furthermore, for any $\mathbf{w}_1, \mathbf{w}_2 \in M$, bilinearity forces $\langle \mathbf{w}_1, \mathbf{w}_2 \rangle \in \mathbb{Z}$. Since $L \subseteq M$ and $\operatorname{rank}(L) = 24$, $M$ is an even integral lattice of rank $24$. ◻

Proof. Suppose, for the sake of contradiction, that there exists a vector $\mathbf{r}\in M$ with $\|\mathbf{r}\|^2=2$.

By Lemma 6, $M \subseteq L^*$. Therefore: $$\begin{equation} \mathbf{r}\in L^*\setminus\{\mathbf{0}\}. \end{equation}$$ The dual Fourier equality condition [eq:dualvanishing] of Corollary 4 evaluated at $\mathbf{k}=\mathbf{r}$ requires: $$\begin{equation} \label{eq:vanishing_at_r} S(\mathbf{r})\widehat f(\mathbf{r})=0. \end{equation}$$ Since $\|\mathbf{r}\|^2=2$, Theorem 2 (item 5) implies that $\mathbf{r}$ is not a zero of $\widehat f$. Because $\widehat f\geq0$ everywhere, it follows that $\widehat f(\mathbf{r})>0$. Consequently, equation [eq:vanishing_at_r] forces: $$\begin{equation} \label{eq:Szero} S(\mathbf{r})=0. \end{equation}$$

On the other hand, we compute $S(\mathbf{r})$ directly from its definition. By Theorem 7, $M$ is an integral lattice. Since $\mathbf{r}\in M$ and each representative $\mathbf{x}_j\in X\subseteq M$, the inner product between them is strictly an integer: $$\begin{equation} \langle\mathbf{r},\mathbf{x}_j\rangle\in\mathbb Z \qquad \text{for every }j \in \{1, \dots, m\}. \end{equation}$$ Therefore, every phase factor in the structure factor evaluates to unity: $$\begin{equation} e^{2\pi i\langle\mathbf{r},\mathbf{x}_j\rangle}=1 \qquad \text{for every }j \in \{1, \dots, m\}. \end{equation}$$ Using the definition of the structure factor [eq:structure]: $$\begin{equation} \label{eq:Sm2} S(\mathbf{r}) = \left| \sum_{j=1}^m e^{2\pi i\langle\mathbf{r},\mathbf{x}_j\rangle} \right|^2 = \left|\sum_{j=1}^m 1\right|^2 = m^2. \end{equation}$$ Because $m \ge 1$, $S(\mathbf{r}) = m^2 \ge 1 > 0$.

Equations [eq:Szero] and [eq:Sm2] contradict each other ($0 = m^2 \ge 1$). Hence, no such vector $\mathbf{r}$ can exist in $M$. ◻

Proof. By Theorem 7, $M$ is an even integral lattice, so its squared norms are even integers. The hard-core exclusion condition rules out $\|\mathbf{w}\|^2 = 0$, and Theorem 9 rules out $\|\mathbf{w}\|^2 = 2$. Thus $\min_{\mathbf{w} \neq \mathbf{0}} \|\mathbf{w}\|^2 \ge 4$. ◻

Proof. The representatives $\mathbf{x}_1,\ldots,\mathbf{x}_m$ define $m$ pairwise disjoint cosets of $L$. Since $X \subset M$, all $m$ disjoint cosets $\mathbf{x}_j + L$ are contained in $M$. Therefore, $[M:L]\geq m$. Using $\mathop{\mathrm{Vol}}(L)=m$ from Lemma 3: $$\begin{equation} \label{eq:upper_squeeze} \mathop{\mathrm{Vol}}(M) = \frac{\mathop{\mathrm{Vol}}(L)}{[M:L]} \leq \frac{m}{m} = 1. \end{equation}$$ ◻

Proof. By Corollary 10, $M$ is a full-rank lattice in $\mathbb{R}^{24}$ with minimum squared norm at least $4$. Open balls of radius $1$ centered at points of $M$ form a non-overlapping sphere packing. By the established dimension-24 sphere-packing theorem of CKMRV , no sphere packing of unit balls in $\mathbb{R}^{24}$ can exceed density $\frac{\pi^{12}}{12!}$. Applying this bound directly to the lattice packing $M$ gives: $$\begin{equation} \frac{\mathop{\mathrm{Vol}}(B_{24}(1))}{\mathop{\mathrm{Vol}}(M)} \leq \frac{\pi^{12}}{12!} = \mathop{\mathrm{Vol}}(B_{24}(1)). \end{equation}$$ Dividing both sides by $\mathop{\mathrm{Vol}}(B_{24}(1))$ yields: $$\begin{equation} \label{eq:lower_squeeze} \mathop{\mathrm{Vol}}(M)\geq1. \end{equation}$$ ◻

Proof. Combining [eq:upper_squeeze] and [eq:lower_squeeze] yields $1 \le \mathop{\mathrm{Vol}}(M) \le 1$, so $\mathop{\mathrm{Vol}}(M)=1$. Substituting this into $\mathop{\mathrm{Vol}}(M) = \frac{m}{[M:L]}$ forces $[M:L]=m$. ◻

Proof. By Theorem 7, $M$ is an even integral lattice of rank $24$. By Theorem 13, it has covolume $1$, so it is an even unimodular lattice. Moreover, Corollary 10 establishes that $\min_{\mathbf{w}\neq\mathbf{0}} \|\mathbf{w}\|^2\geq4$, so $M$ contains no roots of squared norm $2$.

By the classification of positive-definite even unimodular lattices of rank $24$ (Niemeier ), there exist exactly $24$ isometry classes, and the Leech lattice $\Lambda_{24}$ is the unique class with no roots. Therefore: $$\begin{equation} M\cong\Lambda_{24}. \end{equation}$$ ◻

Proof. The quotient group $M/L$ has order $[M:L] = m$. Since the representatives $\mathbf{x}_1,\dots,\mathbf{x}_m$ define $m$ pairwise disjoint cosets of $L$ contained in $M$, they form a complete system of coset representatives for $M/L$. Their union therefore exhausts $M$ completely. ◻

Proof. By definition, $X = \bigcup_{j=1}^m (\mathbf{x}_j + L)$. Since $L \subseteq M$ and every representative $\mathbf{x}_j$ belongs to $M$ by construction, each coset $\mathbf{x}_j + L$ is contained in $M$. Thus $X \subseteq M$.

By Theorem 13, the index satisfies $[M : L] = m$. Because the $m$ points $\mathbf{x}_1, \dots, \mathbf{x}_m$ are pairwise distinct modulo $L$, Lemma 15 establishes: $$\begin{equation} X = \bigcup_{j=1}^m (\mathbf{x}_j + L) \equiv M. \end{equation}$$ By Theorem 14, $M \cong \Lambda_{24}$. Therefore, $X$ is congruent to $\Lambda_{24}$. ◻