On dense tetrahedra in binary sphere packings

This paper considers the density of tetrahedra arising in a specific decomposition of packings of unequal spheres in $\mathbb{R}^3$. It aims to extend a bound obtained in 2D in the 1960s by Florian. The focus is on packings of spheres of sizes $1$ and $\sqrt{2}-1$: the small sphere fits exactly into each octahedral hole of a hexagonal close packing of large spheres, yielding a conjecturally maximally dense packing (for these sizes). The paper slightly improves, by completely different means, the previous best upper bound on the density of such packings. The proof combines geometric insight with challenging interval arithmetic computations, which may be of independent interest.