On a Detail in Hales's "Dense Sphere Packings: A Blueprint for Formal Proofs"

Abstract

In "Dense Sphere Packings: A Blueprint for Formal Proofs" Hales proves that for every packing of unit spheres, the density in a ball of radius $r$ is at most $π/\sqrt{18}+c/r$ for some constant $c$. When $r$ tends to infinity, this gives a proof to the famous Kepler conjecture. As formulated by Hales, $c$ depends on the packing. We follow the proofs of Hales to calculate a constant $c'$ independent of the sphere packing that exists as mentioned in "A Formal Proof of the Kepler Conjecture" by Hales et al..

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.