This paper provides the currently best known upper bound on the density of a packing in three-dimensional Euclidean space of two types of spheres whose size ratio is the largest one that allows the insertion of a small sphere in each octahedral hole of a hexagonal compact packing of large spheres. This upper bound is obtained by bounding from above the density of the tetrahedra which can appear in the additively-weighted Delaunay decomposition of the sphere centers of such packings. The proof relies on challenging computer calculations in interval arithmetic and may be of interest by their own.
Comment: 45 pages, 15 figures, 10 accompanying computer programs