2. The Cohn–Elkies bound
The report uses the linear-programming bound \Delta_d \le \mathrm{LP}_d of Gorbachev and
Cohn–Elkies as an external input. The Lean development proves it, following the original
argument of Cohn and Elkies: for a periodic packing, Poisson summation over the packing lattice
converts a sum of the auxiliary function over differences of centers into a sum over the polar
lattice whose terms are nonnegative, and the term at the origin already gives the bound; general
packings are then approximated by periodic ones. The sphere-packing fundamentals (periodic
packings, their density formula and the passage from arbitrary to periodic packings) were adapted
from the Sphere Packing in Lean project, and Poisson summation for a general lattice of
\mathbb{R}^d was formalized for this purpose. The chapter corresponds to the modules
CohnElkies/SpherePacking/{Basic,Periodic,PeriodicApproximation,CohnElkiesBound}.lean and
CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean.
Throughout, d \ge 1, Lebesgue measure on \mathbb{R}^d is written \operatorname{vol}, and
B(x,r) is the open ball.