Fourier inversion for Schwartz functions (Definition 1.1.2) gives f(0) = \int \widehat f. The integrand is continuous, nonnegative and strictly positive at \xi = 0, so the integral is strictly positive.

The bump CohnElkies.bump is smooth, real, radial, nonnegative and supported in the closed ball of radius 1/2, with positive integral (CohnElkies.integral_bumpReal_pos). Its autocorrelation CohnElkies.autocorrelation is again real and radial, and it vanishes for |x| \ge 1 because the supports of \varphi and of \varphi(x - \cdot) are then disjoint (CohnElkies.autocorrelation_eq_zero). Its Fourier transform is the square (\widehat\varphi)^2 (Definition 1.1.2, CohnElkies.fourier_autocorrelation_apply), which is real and nonnegative because \widehat\varphi is real for the real radial function \varphi, and its value at the origin is (\int\varphi)^2 > 0.

The proof occupies the next chapter. For a periodic packing, Poisson summation over its lattice turns the sum of f over differences of centers into a spectral sum whose terms are nonnegative and whose term at the origin already gives the bound (Theorem 2.3.1); arbitrary packings are approximated by periodic ones (Theorem 2.4.1), giving Theorem 2.4.2 in the form \Delta_d \le \operatorname{vol}(B(0,1/2))\,f(0)/\widehat f(0). The volume of the half ball is v_d/2^d (Definition 1.1.3).

Take the infimum over f \in \mathcal{A}_d in Theorem 1.1.8; the radial reduction Lemma 3.2.9 identifies the radial and the full program.

\mathrm{LP}_d = (v_d/2^d)\inf_f f(0)/\widehat f(0) with (v_d/2^d)^{1/d}\sqrt d \to \sqrt{2\pi e}/2 (Lemma 3.1.8) and \sqrt{2\pi e}/(2\pi) = \sqrt{e/(2\pi)}; the logarithmic forms follow by continuity of \log and \log_2 at the positive limit, and the o(1) forms by taking d-th roots.

Lower bound. By Theorem 4.2.2 there is a sequence \epsilon_d \to 0 such that every F \in \mathcal{A}_d satisfies F(0)/\widehat F(0) \ge (2^d/v_d)\,(\sqrt{e/(2\pi)} - \epsilon_d)^d for all sufficiently large d. Inserting this into Definition 1.1.6 gives \mathrm{LP}_d \ge (\sqrt{e/(2\pi)} - \epsilon_d)^d, hence \liminf_{d\to\infty} \mathrm{LP}_d^{1/d} \ge \sqrt{e/(2\pi)}.

Upper bound. By Theorem 5.5.6, for every small \epsilon > 0 and every large d there is an admissible function of normalized cost at most R_{\epsilon,d}/\sqrt d, where R_{\epsilon,d}/\sqrt d \to \alpha_\epsilon as d \to \infty and \alpha_\epsilon \to 1/\pi as \epsilon \downarrow 0; together with Lemma 3.1.8 this gives \limsup_{d\to\infty}\mathrm{LP}_d^{1/d} \le \sqrt{e/(2\pi)}. In the formalization the two halves are not taken separately: the sandwich argument Theorem 7.6.1 combines the uniform lower bound with the \epsilon-family of upper constructions and yields the limit \inf_{f\in\mathcal{A}_d}(f(0)/\widehat f(0))^{1/d}/\sqrt d \to 1/\pi directly, from which Stirling's formula gives the claim.

Combine Theorem 1.1.9 with Theorem 1.1.10 and Theorem 1.1.11: \mathrm{LP}_d = (\sqrt{e/(2\pi)} + o(1))^d = 2^{-(\frac12\log_2(2\pi/e) + o(1))d}.