Thomson $N=7$, the cap: minimal pair with $t_{01}\le-0.99$ gives $E\ge E(P)$

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.

Let $y$ be admissible and suppose that

1. the pair $(0,1)$ realises the smallest inner product: $t_{01}\le t_{ij}$ for all $i\ne j$;
2. this pair is nearly antipodal: $t_{01}\le-\tfrac{99}{100}$.

Then

This is the cap cell of Case 2 of the proof of the Thomson problem for seven electrons; it is the only cell that contains the pentagonal bipyramid itself (whose poles have $t_{01}=-1$), so the bound is sharp here. The hypothesis that the pair $(0,1)$ minimises the inner products is the minimal-pair normal form: every admissible configuration can be relabelled into it, and relabelling does not change the energy. In the source it follows from a near-sharp typed three-point certificate combined with a rigidity argument and an exact second-order local minimality theorem for $P$.

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).