Thomson $N=7$: cubic lower bound for the energy excess over the pentagonal bipyramid

Let $P=(P_0,\dots,P_6)$ be the pentagonal bipyramid with the regular pentagon $P_k=(\cos\tfrac{2\pi k}5,\sin\tfrac{2\pi k}5,0)$ at indices $k=0,\dots,4$ and the poles $(0,0,\pm1)$ at indices $5,6$; let $\varphi(t)=(2-2t)^{-1/2}$, so that $\|x-y\|^{-1}=\varphi(\langle x,y\rangle)$ for unit vectors, and write $g_{ij}=\langle P_i,P_j\rangle$ and $E(y)=\sum_{i<j}\|y_i-y_j\|^{-1}$. Let $W_{ij}=\varphi(g_{ij})^3$ for $i\ne j$, $W_{ii}=0$, and $\mu_i=\sum_j W_{ij}g_{ij}$.

Let $y=(y_0,\dots,y_6)$ be seven pairwise distinct unit vectors in $\mathbb R^3$, write $h_i=y_i-P_i$ and $\tau_{ij}=\langle y_i,y_j\rangle-g_{ij}$. Then

It follows from the pairwise Taylor/Bregman bound $\varphi(g+\tau)\ge\varphi(g)+\varphi'(g)\tau+\tfrac12\varphi''(g)\tau^2+\tfrac16\varphi'''(g)\tau^3$ on $[-1,1)$ together with the first-order (equilibrium) identity of $P$, which rewrites the linear terms as the $W$/$\mu$ quadratic form.

Formalization Note All named objects (pentBipyramid, coulombEnergy, Base.phi, Reg.W, Reg.muP, Reg.gP, Reg.tau, Reg.Dpair, Reg.Qhess, Reg.Pen, Glue.TubeRigid) come from the platform definition ThomsonN7_core, taken verbatim from the source; R3 is EuclideanSpace ℝ (Fin 3).