Thomson $N=7$: the cap certificate satisfies the cap specification at $a_0=-\tfrac{99}{100}$

Let $\varphi(t)=(2-2t)^{-1/2}$, let $P$ be the pentagonal bipyramid and $E$ the Coulomb energy, and write $c_1=\cos\tfrac{2\pi}5$, $c_2=\cos\tfrac{4\pi}5$. The cap specification at $a_0=-\tfrac{99}{100}$ holds: there are reals $e,\delta,\tau$ and functions $H_A,H_B,H_C:\mathbb R\to\mathbb R$ such that

1. $\tau\le\tfrac1{165000}$ and $E(P)\le e+\delta$;
2. 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$,

where $\mathrm{cls}(i,j)$ is $A$ for the pair $\{0,1\}$, $B$ for pairs meeting $\{0,1\}$ in one point, and $C$ otherwise; 3. $H_A\le\varphi$ on $[-1,a_0]$ and $\varphi(t)-H_A(t)\le\delta\Rightarrow|t+1|\le\tau$ there; 4. $H_B\le\varphi$ on $[-1,1)$ and $\varphi(t)-H_B(t)\le\delta\Rightarrow|t|\le\tau$ there; 5. $H_C\le\varphi$ on $[-1,1)$ and $\varphi(t)-H_C(t)\le\delta\Rightarrow|t-c_1|\le\tau$ or $|t-c_2|\le\tau$ there.

This is the certificate half of the cap cell in the proof of the Thomson problem for seven electrons: combined with the soundness theorem ThomsonN7.Glue.capSpec_sound it gives $E(P)\le E(y)$ on the cap.

Formalization Note Glue.CapSpec and the data of the certificate tc_cap are the platform definitions ThomsonN7_core and ThomsonN7_cap_data_1/2, taken verbatim from the source.