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

TL;DR

This paper refines Hales's proof of the Kepler conjecture by calculating a packing-independent constant, strengthening the original density bound for sphere packings.

Contribution

It computes a universal constant c' in Hales's density bound, independent of specific sphere packings, enhancing the original proof's generality.

Findings

Derived a packing-independent constant c'

Validated the density bound for all sphere packings

Strengthened the formal proof of the Kepler conjecture

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 $\pi/\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..