The 24-cell conjecture in the all-contact case and near D4

The 24-cell conjecture states that every Voronoi cell of a packing of unit balls in R4 has volume at least 8, the volume of the regular 24-cell. We prove it in two cases, with equality only for the D4 root configuration. The first case consists of the cells whose ball touches every ball centred within distance 2√2 of its centre. There the cell is bounded from below by a third-order inclusion–exclusion expansion truncated at radius √2, which is exact at D4. Configurations with 24 contacts are D4 by the uniqueness theorem of de Laat, Leijenhorst and de Muinck Keizer, and for at most 23 contacts we give an exact rational certificate for the second level of the Lasserre hierarchy. The second case is an explicit neighbourhood of D4: 24 other centres have directions within root-sum-square distance 2/5 of a rotated D4 root system and distances from the centre that exceed 2 by at most 3/100 in total, and nothing is assumed about the other centres. This proof combines an inversion hull, a rigidity estimate with slack and an expansion of the truncated volume to second order with explicit remainders, whose constants are certified in exact and in ball arithmetic. We also show that no point inside the ball of radius √2 lies in five of the caps cut off by the Voronoi hyperplanes, and we describe a formalisation in Lean of the reduction of the first theorem to its certificate and of the certificate's arithmetic. Version 2 adds the second case (Section 7) and the formalisation in Lean (Section 8). 28 pages, 5 tables. Supplementary files are deposited separately.