Formal verification of upper bounds on translative packing densities