Thomson $N=7$: a cap specification implies the theorem on the cap

Let $a_0\in\mathbb R$ and suppose the cap specification at $a_0$ holds (reals $e,\delta,\tau$ with $\tau\le\tfrac1{165000}$, $E(P)\le e+\delta$, class minorants $H_A,H_B,H_C\le\varphi$ whose typed pair sum is at least $e$ on minimal-pair configurations with $\langle y_0,y_1\rangle\le a_0$, and whose slack $\varphi-H$ being at most $\delta$ forces the inner product within $\tau$ of $-1$, $0$, or one of $c_1=\cos\tfrac{2\pi}5$, $c_2=\cos\tfrac{4\pi}5$ respectively).

Then for every configuration $y$ of seven distinct unit vectors in $\mathbb R^3$ in which the pair $(0,1)$ realises the smallest inner product and $\langle y_0,y_1\rangle\le a_0$:

2. if $E(y)=E(P)$, then $y_i=g(P_{\sigma(i)})$ for some linear isometry $g$ of $\mathbb R^3$ and some permutation $\sigma$ of $\{0,\dots,6\}$.

Here $P$ is the pentagonal bipyramid with the pentagon at indices $0,\dots,4$ and the poles at $5,6$, and $E(y)=\sum_{i<j}\|y_i-y_j\|^{-1}$.

This is the analytic half of the cap cell: it turns the near-sharp certificate into the sharp bound via tube rigidity of the bipyramid and its exact second-order local minimality.

Formalization Note Glue.CapSpec, Glue.Concl, SphereConfig and pentBipyramid come from the platform definition ThomsonN7_core, taken verbatim from the source.