4. The universal Cohn–Elkies lower bound
By the radial reduction of the preliminaries we may assume that an admissible packing function
F is radial. Let a = (\widehat F(0)/F(0))^{1/d} and h(x) = F(ax). Then
h(0) = \widehat h(0), and g = \widehat h - h is anti-self-Fourier, vanishes at the origin, and
is nonnegative for |x| \ge 1/a. Since \int g = 0, its negative part has mass \|g\|_1/2,
all of which lies in B(0,1/a). Proposition 3.1 shows that every radial Schwartz Fourier
eigenfunction vanishing at the origin, of either eigenvalue, has exponentially little L^1 mass
in B(0,c\sqrt d) when c < 1/\pi; the negative half-mass of g cannot fit inside this ball,
forcing 1/a \ge (1/\pi - o(1))\sqrt d.
The obstruction comes from the Mellin–Fourier identity (9). Lemma 3.2 bounds a normalized Mellin
transform Z on the strip |\operatorname{Im} t| \le \lambda: total L^1 mass controls the
upper boundary, the functional equation controls the lower boundary, and Poisson interpolation
gives \log|Z(s+i\sigma\lambda)| \le H_\sigma(s) \le H_\sigma(0), with
H_\sigma(0) \le \lambda M_\sigma(\log(2\pi c^2) + J_\sigma) + O_\sigma(\log\lambda) by Lemma 3.3.
The sharp constant enters through Lemma 3.4: J_\sigma \to \log(\pi/2) as \sigma \uparrow 1,
so the parenthesized rate tends to \log(\pi^2c^2), negative exactly when c < 1/\pi. Lemmas
3.5 and 3.6 turn this negativity into the interior-mass estimate.
In the formalization the functions of this chapter are the structure
CohnElkies.RadialEigenfunction d ς: a nonzero real radial test function g with
\widehat g = \varsigma g and g(0) = 0, for a unit \varsigma of \mathbb{Z}. The chapter
corresponds to the modules CohnElkies/LowerBound/*.lean; the interior bound of Lemma 3.2 is
proved, as in the report, by mapping the strip onto the upper half-plane and applying the
Poisson inequality for subharmonic functions (the preliminaries chapter), and the limit of Lemma
3.4 by a Frullani-type computation recorded in the final chapter, which also contains an
alternative proof of the Poisson inequality for the strip by Phragmén–Lindelöf.