@YoavKallus You are right. I was conflating computing the number and deciding if it was equal to $\pi/3\sqrt{2}$ (which is the point of the OPs question that these concepts are not the same). You algorithm is exactly right. Optimal packings in a cube where the balls can stick out are an over estimate and optimal packings where the balls don’t stick out is an under estimate. Hence we can compute the optimal packing in the limit to arbitrary accuracy.

As for whether the optimal sphere packing number is computable (before Hale’s proof), there has been a lot of confusion about this. I’ve heard highly qualified logicians say that Kepler’s conjecture is decidable from basically the decidability of RCF. Then similar ideas can be used to compute the optimal ratio. This appears not to be the case: mathoverflow.net/questions/317692/… (However the optimal packing in a cube of fixed size is computable. The issue is that the limit as the cube grows is not obviously computable.)

@KevinBuzzard Yes, $n=7$. I’ve made it explicit now.