Densest packings of two translates of a lattice in four dimensions

Let Λ be a lattice in R4 and b a vector not in Λ such that distinct points of Λ ∪ (Λ + b) are at distance at least 2. We prove that the covolume of Λ is at least 16, with equality only when Λ ∪ (Λ + b) is congruent to √2 D4. Thus no packing of unit balls whose centres form two translates of a lattice is denser than the D4 lattice packing, and every Voronoi cell of such a packing has volume at least 8, the volume of the regular 24-cell. The archive contains the paper (PDF, LaTeX sources with PNG figures, arXiv tarball), the exact enumeration of the polyhedron of two-periodic packings, the integer certificates, and independent checks in C, Julia, Lean 4 and Python. Version 1.1.0 adds the manuscript in the form submitted to Discrete & Computational Geometry, a copy of the d4-voronoi-cells v2.0.0 code (doi:10.5281/zenodo.23240354) under its own licence, a floating-point test of the statements (G) and (C) of that code on two-periodic packings, and a record of two analytic approaches to (G) and (C) with the points where each stops. The general 24-cell conjecture remains open and is not claimed.