\StartTechnicalAppendices \section{Geometric and radial certificates}\label{sec:09-geometric-certificates} This appendix proves Lemma~\ref{lem:li5-weighted-form}, the positivity of the weighted form that Section~\ref{sec:07-lithium-dianion} uses for the lithium dianion. We first fix the conventions for the computer-assisted checks. As in the introduction, a certificate is finite data from which a program verifies a stated inequality. We also call such data a witness. An exact reader is a program that checks a certificate in exact arithmetic. The finite witnesses, polynomial coefficient lists, exact readers and completed execution records used below are retained in the accompanying code/data release. We identify each dataset by its mathematical contents. The checks use exact integers and rationals, including signed floor division. A finite binary64 input denotes its exact dyadic value. Either signed zero denotes zero, and nonfinite inputs are rejected. Write $\operatorname{rn}_{64}$ for nearest binary64 rounding with even ties, followed by this exact interpretation. Integer power comparisons certify all radical enclosures. Locally, Set-up~\ref{setup:execution} means faithful Python integer and rational operations, binary decoding, decompression, file operations and execution records, with assertions enabled and identical input bytes throughout each composed execution. Hashes identify artifacts. They are not substitutes for byte preservation or successful evaluation. The numerical accuracy of the witness-generating program is not used. \subsection{The five-electron weighted form} Several radial estimates below use the following square identity. For $0\le l-3/r+73\ell(\ell+1)/(200r^2)$ at the levels used below. The positive function $r^\mu(1-3r/\mu)$ with $\mu=1$ for $\ell=0$ and $\mu=9/5$ for $\ell=1$ gives the respective origin trace coefficients $680/37$ and $808/23$ through \eqref{eq:geometric-certificates-square}. On $r\ge200$ the $s$ tests satisfy $r^2W>28$, and the $p$ test at $e=-7.119$ satisfies $r^2W>63/25$. These follow by inserting the constant end values $h_s=-23.058$, $h_p=5$ in \eqref{eq:geometric-certificates-li-potential} and using $r^2/p>999/1000$, $6r/p\le3/100$. The tail functions $r^{-7}$ and $r^{-9/5}$ give trace coefficients $7/400$ and $9/2000$, respectively. Here is the finite algebraic test for the lithium radial datasets. On a cell $[l,u]$ set $\delta=u-l$, $t=(r-l)/\delta$, $J=r^2p^2$ and $H=2JW_{e,\ell,h}$. Each cell contains no interior field knot. There are two types of barrier: \begin{align*} b=P(t)/r:&\quad R_Q=H-p^2[(r/\delta)P'-P+P^2],\qquad W-\tfrac12(b'+b^2)=R_Q/(2J),\\ b=F'(t)/(\delta F(t)):&\quad R_F=HF-JF''/\delta^2,\qquad W-\tfrac12(b'+b^2)=R_F/(2JF). \end{align*} The fixed polynomial coefficients are in $10^{-18}\mathbb Z$ and their cell endpoints are in $10^{-6}\mathbb Z$. The accompanying complete coefficient lists prove positivity of $R_Q$, or of both $F,R_F$, using identities of the form \begin{equation}\label{eq:geometric-certificates-positive-polynomial} D T(t)=c+\sum_{a_k\ge0}a_kt^k +\sum_{a_k<0}(-a_k)(1-t^k),\qquad D,c>0. \end{equation} All quantities are integers after clearing denominators. Coefficient convolution and differentiation check the identity. Each summand on its right is nonnegative on $[0,1]$. This gives a positive residual on the whole cell, without a rounding error or a sampled sign test. The fixed lists have the coverage in Table~\ref{tab:geometric-certificates-lithium-radial-cells} and the junction properties described below. \begin{table}[ht] \centering\small \caption{Polynomial cells for the lithium radial bounds.} \label{tab:geometric-certificates-lithium-radial-cells} \begin{tabular}{cclrr} field&$\ell$&level and interval&type&cells\\\hline $h_s$&0&$-10.624$, $[1/40,200]$&$Q$&63\\ $h_s$&0&$-7.793$, $[1/40,97/100]$&$F$&17\\ $h_s$&0&$-7.793$, $[98/100,200]$&$F$&44\\ $h_p$&1&$-7.119$, $[1/40,200]$&$Q$&69 \end{tabular} \end{table} The $Q$ rows match the endpoint values of $rb$, and hence of $b$. For the $F$ rows the complete rational junction list gives $b(l-)-b(l+)\ge0$. Such downward jumps contribute nonnegative traces in \eqref{eq:geometric-certificates-square}. At the right endpoint the values of $200b(200)$ are, in the order ground $s$, right-hand second $s$, and $p$, \[ \frac{1056766439842756911}{125000000000000000},\qquad \frac{655514571348203063000000000}{81169011805581996247117017},\qquad \frac{4352114208735658733}{10^{18}}. \] All are positive and attach to the positive tail traces. For the $p$ rows the initial value is $r_*b(r_*)=1756521739130434782/10^{18}\le202/115 =2r_*(808/23)$. For the left-hand second $s$ rows the initial value is at most $34/37=2r_*(680/37)$. The ground $s$ certificate also contains a degree-$10$ origin polynomial $g$ with $g(0)=0$, $g'(0)=1$, $g''(0)=-6$. Its two identities \eqref{eq:geometric-certificates-positive-polynomial} certify positivity of $g(r_*t)/(r_*t)$ and of \[ \frac{N(r_*t)g(r_*t)-D_0(r_*t)g''(r_*t)}{t^2},\qquad N(r)=2rp(r)(10499/1000)-12p(r)+2r,\quad D_0(r)=rp(r)^2. \] The numerator is divisible by $t^2$. Since $N=2D_0W_{-10.624,0,h_s}$, these identities give the required origin differential inequality. The listed rational endpoint comparison is $r_*g'(r_*)/g(r_*)>925444130490188736/10^{18}$, the initial core value. It is a downward junction, so the origin attaches without a negative trace. For the second $s$ level put $r_c=97/100$ and impose $y(r_c)=0$. The right-side seed is a degree-$10$ polynomial $g_c(x)$, $x=r-r_c$, on $0\le x\le1/100$, with $g_c(0)=0$, $g_c'(0)=1$. Its two retained positive identities concern $g_c(t/100)/(t/100)$ and \[ \frac{H(97/100+t/100)g_c(t/100) -J(97/100+t/100)g_c''(t/100)}t. \] They prove a positive function and a nonnegative differential residual, and the first right-side junction is downward. At the cut there is no boundary debit: for $y(r_c)=0$, $|y(r_c+x)|^2/x\le\int_{r_c}^{r_c+x}|y'|^2\to0$, while $g_c'/g_c=1/x+O(1)$. Hardy's inequality also controls the square term. Thus the two sides give nonnegativity on this single trace kernel. These identities, all coefficients of the two seeds, and every junction comparison are the fixed lithium radial certificate data in the code/data release. The checks just described involve the complete lists, of lengths $63,17,44,69$, and their seed identities. Summation of \eqref{eq:geometric-certificates-square} proves the ground $s$ and $p$ floors and the second $s$ index bound. The latter follows because a two-dimensional negative space would meet the one-trace kernel nontrivially. \emph{The third $s$ level.} Define \[ V_*(r)=\frac{r-27}{r(r+3)^2},\qquad g_*(r)=\frac{r(10r^2-45r+27)}{(r+3)^4},\qquad E_*(r)=\frac{47}{8}+\frac{27r-29}{(r+3)^2}+\frac1{r^2+2}. \] Direct differentiation gives $-g_*''/2+V_*g_*=0$. Its only positive zeros are $(45\pm3\sqrt{105})/20$. The square identity on the three intervals between these zeros proves nonnegativity on the kernel of the two traces, hence index at most two. Moreover $p(W_{-7,0,h_s}-V_*)=E_*-h_s$. The exact bounds in Table~\ref{tab:geometric-certificates-lithium-third}, obtained from the field knots, prove $E_*-h_s\ge1/200$ on the entire half-line. \begin{table}[ht] \centering\small \caption{Bounds for the third lithium $s$ level.} \label{tab:geometric-certificates-lithium-third} \begin{tabular}{c|cc} interval&upper bound for $h_s$&lower bound for $E_*$\\\hline $[0,57/100]$&$489/250$&$191/72$\\ $[57/100,5/4]$&$1169/250$&$191/40$\\ $[5/4,2]$&$6059/1000$&$49/8$\\ $[2,3]$&$6807/1000$&$55/8$\\ $[3,9]$&$7289/1000$&$527/72$\\ $[9,12]$&$287/40$&$2587/360$\\ $[12,18]$&$687/100$&$55/8$\\ $[18,22]$&$1209/200$&$51/8$\\ $[22,\infty)$&$5429/1000$&$47/8$ \end{tabular} \end{table} For the lower bounds, discard $1/p$ and use $((27r-29)/(r+3)^2)'=(139-27r)/(r+3)^3$. Its minimum on a finite interval is at an endpoint. For the first and last rows use respectively $(27r-29)/(r+3)^2\ge-29/9$ and $\ge0$. Therefore $W_{-6.995,0,h_s}\ge V_*$, which proves the stated index bound. Finally the knotwise maximum of $h_s-h_p$ is $.161$, so $K_1-h_s\ge-7.119-.161=-7.280$. Increasing $\ell\ge1$ adds a nonnegative centrifugal term and proves the remaining assertions. \end{proof} \begin{lemma}[Five-electron weighted form]\label{lem:li5-weighted-form} Assume Set-up~\ref{setup:execution} for the specified Li5 certificate executions. Set $U_0=-37431243/5000000$ and \[ (\omega_1,b_1,\delta_1)=(83/250,26/25,129/40),\qquad (\omega_2,b_2,\delta_2)=(527/1000,103/50,3469/5000). \] Write $s_+=\max(s,0)$ for real $s$. For $t\ge0$ and $a\in\{1,2\}$ put $B_a(t)=(t-b_a)_+^2-\min(t/b_a,1)/(2\delta_a)$. For $x=(x_1,\ldots,x_5)$ set $r_i=|x_i|$, $d_{ij}=|x_i-x_j|$, let $q_1\le\cdots\le q_5$ be the ordered radii, and put $V(q)=\omega_1B_1(q_1)+\omega_2B_2(q_2)$. Then every compactly supported antisymmetric $u\in H^1((\mathbb R^3)^5;\mathbb C^{32})$ satisfies \begin{multline*} \frac12\sum_{i=1}^5\int(r_i^2+2)|\nabla_i u|^2+ \int\left[ \sum_{i.105140625$ and $L_+>.99327084375$. The inner coefficients of $\mathcal V_5$ exceed $3A_*/2-2A_*^3+3L_->.696283375$, and the outer coefficients exceed $3B_*-3B_*^3+2L_+>3.1406086875$. This proves the first bound in \eqref{eq:geometric-certificates-cheap}. For the second, put $c(z)=\min\{1,[2(1-z)]^{-1/2}\}$ on $[-1,1)$ and $c(1)=1$. The maximum of $1+t^2-2tz$ on $0\le t\le1$ is $\max(1,2(1-z))$, so $(d_{ij}^*)^{-1}\ge\min(q_i^{-1},q_j^{-1})c(n_i\cdot n_j)$. For $2\le\nu\le5$, the tangent to $[2(1-z)]^{-1/2}$ at $z=-1/(\nu-1)$ lies below $c$: its maximum is $\tfrac32\sqrt{(\nu-1)/(2\nu)}\le1$. For $\nu$ unit vectors, $\sum_{it\}$ gives their successive increments divided by $q_2,q_3,q_4,q_5$, which are exactly $t_i^*$. On a box $Q=\prod_i[l_i,h_i]$, $0\le l_i0$ and $\Lambda\ge\lambda_{\max}(\mathsf D^{-1/2}\mathsf A\mathsf D^{-1/2})$, the symmetric choice $\mathsf B=t\mathsf A$, retaining the normal-component squares, gives \begin{equation}\label{eq:geometric-certificates-collective} T_{\mathsf D}+U_{\mathsf A}\ge t\operatorname{tr}\mathsf A -\frac{\operatorname{tr}\mathsf D}{8t^2}(2t+t^2\Lambda-1)_+^2. \end{equation} To verify the penalty, write $U=U_{\mathsf A}\ge0$. The square expansion is bounded below by $t\operatorname{tr}\mathsf A+(1-2t-t^2\Lambda)U +2t^2U^2/\operatorname{tr}\mathsf D$. Here $\mathsf A\mathsf D^{-1}\mathsf A\le\Lambda\mathsf A$ and weighted Cauchy--Schwarz bounds the retained normal squares. Minimizing this quadratic for $U\ge0$ proves \eqref{eq:geometric-certificates-collective}. For $\rho_i\ge0$, $\sum_i\rho_i\le1$, and $0\le t_i^2\le d_i/2$, one has \begin{equation}\label{eq:geometric-certificates-conditional} T_{\mathsf D}+U_{\mathsf A}\ge\sum_i(2t_i\sqrt{\rho_i\mathsf A_{ii}/2}-t_i^2), \qquad t_i\ge0. \end{equation} For a normalized slice in the $i$th angular variable let $m_i=|\langle n_i\rangle|<1$. Conditional averaging of a positive Gram form gives $\langle U_{\mathsf A}\rangle\ge\mathsf A_{ii}(1-m_i^2)/2$. Integration by parts against a coordinate on $S^2$, followed by Cauchy--Schwarz, gives $\int|\nabla_i\chi|^2\ge m_i^2/(1-m_i^2)$ on the normalized slice. Set $v=1-m_i^2$. The contribution with weight $\rho_i$ is at least $(\rho_i\mathsf A_{ii}/2)v+(d_i/2)(v^{-1}-1)$. For $00$ and a symmetric rational $M\ge0$ with $M_{ij}=\lambda_{ij}^3$ off the diagonal. Put $\eta_i=(M_{ii}+\sum_{j\ne i}M_{ij})/2$, $u_{ij}=(2+(x_i^*)^2+(x_j^*)^2)^{1/3}$, and choose rational \[ 0\le\eta_{ij}\le \frac{\lambda_{ij}}{3(2+h_i^2+h_j^2)^{1/3}}. \] The common part of the support is \begin{align} P_0(q)={}&\sum_{i0$, and a positive vector $z^*$, all rational. Put $y_i^*=h_i/\sqrt{k_i}$ and $\mathsf C_{ij}=M_{ij}y_i^*y_j^*$. Choose a rational $\Lambda$ bounding either $\operatorname{tr}\mathsf C$ or $\max_i(\mathsf Cz^*)_i/z_i^*$, and set $v_*=2t+t^2\Lambda/\alpha-1$. If every $l_i>0$, choose \[ P_{\rm en}\ge \frac{\alpha\sum_i\theta(1+2/l_i^2)}{8t^2}(v_*)_+^2; \] if some $l_i=0$, require $v_*\le0$ and put $P_{\rm en}=0$. Add $t\sum_i M_{ii}q_i^2-P_{\rm en}$. The matrix $\mathsf C$ is nonnegative entrywise and positive semidefinite. Its largest eigenvalue is bounded by its trace and by the displayed positive-vector bound: apply the eigenvector equation at an index maximizing the absolute component divided by $z_i^*$. The function $r/\sqrt{\theta(1+2/r^2)}$ is increasing, so the same eigenvalue bound holds at every point of the box. Formula \eqref{eq:geometric-certificates-collective} with the actual kinetic diagonal $\alpha\operatorname{diag}(\theta(1+2/q_i^2))$ proves this recovery. When a lower endpoint is zero, the verified inequality $v_*\le0$ removes the penalty without an infinite endpoint estimate. For the affine recovery choose $0<\alpha\le1$ and any rational matrix $F$ satisfying, with $X=\operatorname{diag}(x_i^*)$ and $\mathsf D=\alpha\operatorname{diag}(k_i)$, \[ \mathsf D-F^T(\mathsf D+XMX)F\ge0. \] Add $\operatorname{tr}(\mathsf D(F-I))+\sum_i(F^TXM)_{ii}q_i$. To prove this, set $E=XF$ and $Y=F^T\mathsf D+E^TMR$. The constraint implies $Y^T\mathsf D^{-1}Y\le\mathsf D+RMR$: stack $\mathsf D^{1/2}F,M^{1/2}E$ and use that a matrix whose column Gram matrix is at most $\mathsf D$ becomes a contraction after multiplication by $\mathsf D^{-1/2}$. For $\mathsf B=Y-\mathsf D$ this is precisely the hypothesis of \eqref{eq:geometric-certificates-matrix-completion}, whose trace is the asserted affine function. No symmetry of $F$ is used. \emph{Pair recoveries.} For the collective and affine recoveries, the fraction $1-\alpha$ of the reserved kinetic energy can be used as follows. An unused pair contributes zero. For a used pair require $\alpha<1$ and $l_i,l_j>0$, and choose rational $b_{ij}^*>0$, $\kappa_{ij}>0$, $\tau_{ij}\ge0$. Choose $00$. Define $z_{ij}^*$ as the minimum of $z^2$ on $I_{ij}$ if $p_{ij}^*\ge0$, and its maximum otherwise. The allowed rational pair constant is \begin{equation}\label{eq:geometric-certificates-pair-gain} 0\le g_{ij}\le\max\left\{0, \frac{\kappa_{ij}\tau_{ij}}2+ \frac{b_{ij}^*p_{ij}^*z_{ij}^*}{b_{ij}^*+p_{ij}^*}\right\}. \end{equation} Indeed the exact remainder in \eqref{eq:geometric-certificates-coulomb-tangent} can be written \[ \frac{\lambda_{ij}^3}{2} \frac{d_{ij}^*+2d_*}{d_{ij}^*(d_{ij}^*+d_*)^2}((d_{ij}^*)^2-d_*^2)^2. \] The prefactor decreases as $d_{ij}^*$ increases. Replacing $d_{ij}^*$ by $q_i+q_j$, and then using the stated endpoint bounds, puts this remainder above $b_{ij}^*(n_i\cdot n_j-z_{ij}(q))^2$. Clipping the center decreases distance from every point of $[-1,1]$. Allocate $(1-\alpha)k_i/4$ of the $i$th kinetic coefficient to each incident pair, scaling the two coefficients down together if their sum exceeds $\kappa_{ij}$. Each electron occurs in four pairs, so the allocations do not exceed the available kinetic form. With $\widehat z=z_{ij}(q)$, $v_{ij}=n_i\cdot n_j$ and \[ \sigma_{ij}=\frac{(1+\tau_{ij})b_{ij}^*\widehat z}{b_{ij}^*+p_{ij}^*}, \qquad F_{ij}(v_{ij})=\exp(-\tau_{ij}v_{ij}^2/2+\sigma_{ij}v_{ij}), \] the angular square identity bounds the pair form below by \[ \frac{\kappa_{ij}\tau_{ij}}2+ \frac{b_{ij}^*p_{ij}^*\widehat z^2}{b_{ij}^*+p_{ij}^*} +\left(b_{ij}^*-\frac{\kappa_{ij}(3\tau_{ij}+\tau_{ij}^2)}2\right) \left(v_{ij}-\frac{b_{ij}^*\widehat z}{b_{ij}^*+p_{ij}^*}\right)^2. \] This follows by differentiating $F_{ij}$ on each sphere and using $1-v_{ij}^2\le1$ in the negative square term. The last coefficient is nonnegative, and the original pair form is also nonnegative. Minimizing over the center interval proves \eqref{eq:geometric-certificates-pair-gain}, for either sign of $p_{ij}^*$. \emph{Integer enclosures and scalar signs.} Each support just constructed is separable quadratic. Lower its constant, linear and quadratic coefficients separately to rational values and write the result as $P_Q(q)=c_Q+\sum_i(m_{Qi}q_i+v_{Qi}q_i^2)$. This remains a lower support because $q_i,q_i^2\ge0$. The exact reader uses the scale $S_*=2^{160}$. An integer interval $[L,H]$ denotes $[L/S_*,H/S_*]$. Rational inputs are enclosed by floor and ceiling. Products use the four endpoint products with outward rounding, and division requires a positive lower denominator. Squares include zero when the interval does. Square-root endpoints are certified by comparisons with $LS_*,HS_*$, and cube-root endpoints by comparisons with $LS_*^2,HS_*^2$. Thus the radical bounds are integer inequalities. Even a dyadic input finer than $2^{-160}$ is enclosed outward. Induction over the finite expression proves inclusion with all rounding errors accounted for. The reader requires positive lower pivots in interval symmetric elimination of $M$ and, for an affine recovery, of $\mathsf D-F^T(\mathsf D+XMX)F$. Each trailing interval contains the exact Schur complement, since division has a positive pivot. Triangular congruence then proves positivity of the exact matrices. A zero-containing pivot or an inconclusive domain or sign check rejects the record. The curvature $\eta_{ij}$ is the lower enclosure endpoint of its bound. For collective recovery the reader takes the smaller of upward bounds for the trace and the positive-vector expression, and an upward bound for $P_{\rm en}$. For pair gains it checks every displayed constraint and takes a downward bound in \eqref{eq:geometric-certificates-pair-gain}. If its lower distance enclosure is zero, $1/\lambda_{ij}$ is an admissible positive $d_-$. The implemented bound with zero in the numerator is smaller and remains sufficient. Unused pairs require zero $\tau_{ij}$ and contribute zero. For each coordinate and field $h\in\{h_s,h_p\}$ the reader obtains a rational lower bound $\mu_{i,h}$ for \[ \min_{l_i\le r\le h_i} \left[m_{Qi}r+v_{Qi}r^2+h(r) +\mathbf1_{\{i=1\}}\omega_1B_1(r) +\mathbf1_{\{i=2\}}\omega_2B_2(r)\right]. \] It splits at every field knot and the moment kinks $b_1,b_2$. On each segment the expression is $\mathfrak a r^2+\mathfrak b r+\mathfrak c$. Both endpoints are evaluated; when $\mathfrak a>0$, the vertex value $\mathfrak c-\mathfrak b^2/(4\mathfrak a)$ is also included if $-\mathfrak b/(2\mathfrak a)$ lies in the segment. With interval coefficients the vertex is included whenever its enclosure intersects the segment. If the enclosure of $\mathfrak a$ straddles zero, natural interval evaluation on the entire segment is included; if its upper endpoint is nonpositive, endpoints suffice. Taking the least lower endpoint over all these candidates proves $\mu_{i,h}$ without missing a minimum. For each marked index $j$ in the record, the test is \begin{equation}\label{eq:geometric-certificates-marked-test} c_*+c_Q+\mu_{j,h_p}+\sum_{i\ne j}\mu_{i,h_s}>\varepsilon_*. \end{equation} The reader implements it by a signed integer lower numerator strictly greater than $\lceil S_*/100000\rceil$. \emph{The tree and its implementation.} The fixed lithium witness starts with the eight bytes \texttt{LI5AF001} and the binary64 value $1280$. Its root is $[0,1280]^5$, with all five marks active. A node starts with \texttt{N}, has at most five acceptance records, and supplies for each a nonempty subset of its remaining marks. Each subset is removed after its successful scalar tests. If marks remain, a split at coordinate $\iota$ and exact dyadic $l_\iota<\mu\lceil2^{160}/100000\rceil. \] These are results of the complete evaluations whose exact input, reader, and producer-to-consumer records are retained in the code/data release. The execution assumptions stated at the beginning of this appendix apply to the actual linked bytes and runs. The enclosure and implementation arguments above make these evaluations proofs of all finite support and marked-sign predicates. The witness generator's floating calculations are not premises. \emph{Scalar closure on all radii.} For $03/20$. Nonnegative reciprocal and kinetic terms preserve this lower bound. Enlarge $G$ by its maximum with $G_\infty$ on the compact cone and use $\max(-3\sum_iq_i,G_\infty)$ outside it. The field table gives $h_s,h_p\ge-24$ and $h_s+3r/20,h_p+3r/20\ge0$. At knots $60,130,200$ the respective smallest latter values are $8.407,8.016,6.942$. All earlier knot values are nonnegative, and the affine and constant continuations preserve these estimates. Completing the square gives \[ \omega_a B_a(r)-6r\ge -6b_a-9/\omega_a-\omega_a/(2\delta_a), \] which is greater than $-34$ for $a=1$ and $-30$ for $a=2$. Since $c_*>-31$, when $q_5\ge1280$ every marked scalar expression with $G_\infty$ is greater than $-31-58-54+(3\cdot1280/20-24)=25$. Thus \eqref{eq:geometric-certificates-all-marks} holds on the entire cone. For the all-$s$ expression, $h_p-h_s\le.094$ on $[0,130]$, by the knot differences. Since $e_s-e=.119$, using mark $1$ proves \begin{equation}\label{eq:geometric-certificates-all-s} G(q)+e_s-2U_0-15/8+V(q)+\sum_i h_s(q_i)\ge\varepsilon_* \end{equation} when $q_1\le130$. If $q_1\ge130$, both functions $\omega_aB_a(r)-6r$ increase there, and their values at $130$ exceed $41351/10$ and $72841/10$. The all-$s$ expression is then greater than $(41351+72841)/10-120-31>11000$. This proves \eqref{eq:geometric-certificates-all-s} everywhere needed. \emph{The fermionic weighted form.} Pass to reduced radial measure by \[ \psi(r,n,\sigma)=\Bigl(\prod_i r_i\Bigr) u(r_1n_1,\ldots,r_5n_5,\sigma), \] where $\sigma\in\{1,2\}^5$ indexes the spin components. This is unitary and preserves antisymmetry. For one coordinate, \[ \frac12\int p|\partial_r\psi-\psi/r|^2 =\frac12\int p|\partial_r\psi|^2+\int|\psi|^2, \] since $p'/(2r)=1$. The original constant $-15/2$ therefore becomes $-5/2$. Allocating $-1/8$ to each of the five radial forms leaves $-15/8$. Split the angular kinetic energy into shares $1-\theta$ and $\theta$, and apply the full-angular bound $\mathcal A(q)\ge G(q)$ before any angular projection. The left side in the statement is bounded below by \[ \sum_i\langle\psi,K_{L_i}\psi\rangle+ \int [G(q)-2U_0-15/8+V(q)]|\psi|^2, \] where $K_{L_i}$ denotes the angular direct sum of the $K_\ell$ in the $i$th coordinate. This new form commutes with every labeled angular projection. In a tuple $(\ell_1,\ldots,\ell_5)$ having a nonzero angular momentum, choose one such label $m$, independently of the radii. Subtract $h_p(r_m)$ from its operator and $h_s$ from the other four. By Lemma~\ref{lem:geometric-certificates-lithium-radial}, the marked energy is at least $-7.119$. Each unmarked non-$s$ operator is at least $-7.793$. For an $s$ operator, let $Q_b$ be the spectral projection of $K_0-h_s$ onto $(-\infty,-7.793)$. Then \[ K_0-h_s\ge-7.793+(-10.624+7.793)Q_b. \] The radial rank of $Q_b$ is at most one, and its spin-inclusive rank at most two. The true $s$ labels remain antisymmetric in radial and spin variables, so their total occupation of this subspace is at most two. The four unmarked energies are therefore at least $2(-10.624)+2(-7.793)$. Together with the marked energy they give $e$. The fixed labeled radius $r_m$ is some $q_j$, so the five inequalities \eqref{eq:geometric-certificates-all-marks} restore the fields and give $\varepsilon_*\|\psi\|^2$ on this tuple. No field is assigned to a differential operator according to radial rank. In the all-$s$ tuple let also $Q_c$ project below $-7$. Its radial rank is at most two by the stronger bound at $-6.995$. Spectral calculus gives \[ K_0-h_s\ge-7+(-7.793+7)Q_c+(-10.624+7.793)Q_b. \] The spin-inclusive occupation bounds are four and two. Thus the five one-body energies sum to at least $2(-10.624)+2(-7.793)-7=e_s$, and \eqref{eq:geometric-certificates-all-s} gives the same final bound. Finally the angular constant test in $\mathcal A(q)\ge G(q)$ gives \[ -3\sum_iq_i\le G(q)\le \sum_{i