7.7. The Cohn–Elkies bound is proved🔗

The report cites \Delta_d \le \mathrm{LP}_d as an external input. The formalization proves it, via Poisson summation for periodic packings and the reduction of arbitrary packings to periodic ones; see the chapter on the Cohn–Elkies bound (Theorem 2.4.2 and Theorem 1.1.8). The sphere-packing definitions and the periodic-packing theory were adapted from the Sphere Packing in Lean project.