Thomson $N=7$, slab 1: minimal pair with $t_{01}\in[-\tfrac{99}{100},-\tfrac{49}{50}]$ gives $E>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. $-\tfrac{99}{100}\ \le\ t_{01}\ \le\ -\tfrac{49}{50}$.

Then

This is slab 1 of the five slabs that, together with the cap $t_{01}\le-\tfrac{99}{100}$ and Case 1 (all $t_{ij}\ge-\tfrac9{10}$), cover all configurations in the proof of the Thomson problem for seven electrons. 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 each slab is handled by its own typed three-point certificate with margin about $2.6\cdot10^{-6}$.

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