Thomson $N=7$, Case 1: no near-antipodal pair gives $E\ge E(P)+3\cdot10^{-4}$

Let $P=(P_0,\dots,P_6)$ be the pentagonal bipyramid of the mission (the poles $(0,0,\pm1)$ and the regular pentagon $(\cos\tfrac{2\pi k}{5},\sin\tfrac{2\pi k}{5},0)$, $k=0,\dots,4$), and for a configuration $y=(y_0,\dots,y_6)$ write

for its Coulomb energy. A configuration is admissible if its seven points lie on the unit sphere $S^2\subset\mathbb R^3$ and are pairwise distinct. Write $t_{ij}=\langle y_i,y_j\rangle$ for the pairwise inner products.

If $y$ is admissible and all its pairwise inner products satisfy $t_{ij}\ge-\tfrac{9}{10}$ for $i\ne j$, then

This is Case 1 of the proof of the Thomson problem for seven electrons: configurations without a near-antipodal pair have energy strictly above that of the pentagonal bipyramid, with an explicit margin. In the source it is obtained from a single degree-5 three-point semidefinite certificate together with a polynomial minorant of $t\mapsto(2-2t)^{-1/2}$.

Formalization Note Points live in EuclideanSpace ℝ (Fin 3) and the energy, admissibility and $P$ are the shared definitions coulombEnergy, IsAdmissible and pentagonalBipyramid of Def_ThomsonProblem_defs; the inner product is written inner ℝ (y i) (y j).