\section{Proofs deferred from the main text}\label{sec:13-deferred-proofs} This appendix contains the proofs deferred from Sections~\ref{sec:03-removal}, \ref{sec:05-helium-monoanion} and~\ref{sec:06-lithium-binding}. Each proof uses the notation of the section in which its statement appears. \subsection{The regional lower bound}\label{sec:13-deferred-proofs-regional} \begin{proof}[Proof of Lemma~\ref{lem:regional-bound}] \emph{Angular repulsion.} For positive radii and directions $n_i,n_k\in S^2$, maximizing $1+\tau^2-2\tau z$ over $0\le\tau\le1$ gives \[ \frac1{|r_in_i-r_kn_k|} \ge\min\{r_i^{-1},r_k^{-1}\}\,c(n_i\cdot n_k). \] Let $2\le h\le N$ be an integer and let $n_1,\ldots,n_h$ be directions. Consider the tangent to the convex function $[2(1-z)]^{-1/2}$ at $z=-1/(h-1)$. By convexity, this tangent lies below the untruncated function. Its maximum on $[-1,1]$ is $\frac32\sqrt{(h-1)/(2h)}$, which is at most $1$ exactly when $h\le9$. Hence the tangent lies below $c$. Since $0\le|\sum_in_i|^2=h+2\sum_{i0$, \[ \frac1t-\frac{\sigma^2}{t+R}+\frac{(\sigma-1)^2}{R} =\frac{((\sigma-1)t-R)^2}{Rt(t+R)}\ge0 . \] For a three-dimensional function $w$ vanishing on $\{|x|\le R\}$, apply this inequality to its reduced radial slices $rw$ and discard the nonnegative angular kinetic energy. Dirichlet form density extends the bound to all such $H^1$ functions, componentwise and on almost every slice in the other variables. \emph{Assembly.} Recall that the $j$ electrons with radii below $b$ are the core electrons and the other $N-j$ are the outer electrons. By Theorem~\ref{thm:hydrogen}, the kinetic and nuclear terms of each core electron contribute at least $-Z^2/2$. We drop the repulsion among core electrons. Each pair of one core electron and one outer electron satisfies \[ \frac1{|x_i-x_{\mathrm{core}}|} \ge\frac1{r_i+b}\ge\frac{R}{(R+b)r_i}. \] Apply the radial bound with the charge $\kappa$ to each outer electron. This leaves the potential $-(Z-\kappa)/r_i$. Write $t_i=R/r_i\in(0,1]$ for the inverse scaled radius of the electron. The remaining potential of the outer electrons is bounded below by \[ \frac1R\left[ \sum_{i0$, the trial function is $\psi=e^{-\alpha s}C\chi/(\pi\sqrt{\mathcal N})$. Its second weak derivatives and its Coulomb potential times $\psi$ are bounded by a polynomial times $e^{-\alpha s}(1+r_1^{-1}+r_2^{-1}+d^{-1})$, which is square integrable. Hence $\psi$ belongs to $D(\AtomH{2}{2})$. Its spatial factor is symmetric and rotationally invariant. We now list the integrals and error bounds used in this calculation. For nonnegative integers $p,j,k$, put $m=p+j+k$. Odd $j$ gives zero. For even $j$, \[ \mathcal J(s^p\xi^jd^k) =\frac{2(m+2)!}{(j+1)(j+k+2)g^{m+3}},\qquad \mathcal K(s^p\xi^jd^k) =\frac{(m-1)!}{g^m} 2\int_0^1\int_x^1\frac{x^jy^{k-1}}{1-x^2}\,dy\,dx . \] The second formula is used only for $m>0$. For $k>0$, integration in $y$ and finite geometric sums reduce its angular integral to rational numbers and $\log2$. For $k=0$ that integral is $\pi^2/4-2\sum_{h=0}^{j/2-1}(2h+1)^{-2}$, with an empty sum when $j=0$. For $\tau=-2903724/10^6$, the polynomial obtained by clearing the denominator in the residual is \begin{align*} \mathcal R={}&D[-C_{ss}-C_{\xi\xi}-C_{dd} +2\alpha C_s-(\alpha^2+\tau)C] -4sdC_s+4(\alpha-2)sdC+4\xi dC_\xi\\ &-2(s^2-\xi^2)C_d-2s(d^2-\xi^2)C_{sd} +2\alpha s(d^2-\xi^2)C_d -2\xi(s^2-d^2)C_{\xi d}+(s^2-\xi^2)C . \end{align*} The Cartesian chain rule gives $(\AtomH{2}{2}-\tau)(e^{-\alpha s}C\chi) =e^{-\alpha s}\mathcal R\chi/D$. Put $\mu=\langle\psi,\AtomH{2}{2}\psi\rangle$, $v=\|(\AtomH{2}{2}-\mu)\psi\|^2$, and $m_j=\|r_1^{j/2}\psi\|^2$ for $0\leq j\leq16$. Consequently \[ \mu=\tau+\frac{\mathcal J(C\mathcal R)}{\mathcal N},\qquad v=\frac{\mathcal K(\mathcal R^2)}{\mathcal N}-(\mu-\tau)^2, \qquad m_j=\frac{\mathcal J(DC^2((s+\xi)/2)^j)}{\mathcal N}. \] All these expressions are finite. Polynomial multiplication and the displayed monomial integrals were evaluated exactly. To enclose the two constants in $v$, the calculation used \[ \ell=2\sum_{b=0}^{31}\frac1{(2b+1)3^{2b+1}},\qquad A(x)=\sum_{b=0}^{31}\frac{(-1)^bx^{2b+1}}{2b+1}, \] \[ \ell<\log2<\ell+\frac{2}{65\,3^{65}(1-1/9)},\qquad A(x)\leq\arctan x\leq A(x)+\frac{x^{65}}{65}, \quad x\in\{1/5,1/239\}, \] and $\pi=16\arctan(1/5)-4\arctan(1/239)$. Signed rational substitution gives an upper bound $\bar v\geq v$ with the following recorded enclosures: \begin{align*} -\frac{29037243720149832}{10^{16}} &\leq\mu<-\frac{29037243720149831}{10^{16}},\\ 0\leq v\leq\bar v&<\frac{12177071684819}{10^{20}},\\ -\frac{29037246736334271}{10^{16}} &\leq\mu-\frac{\bar v}{-5/2-\mu} <-\frac{29037246736334270}{10^{16}} . \end{align*} \emph{The neutral level and its gap.} Write $h=-\Delta/2-2/r$, including the two spin copies. By Theorem~\ref{thm:hydrogen}, $h_1+h_2\geq-5/2$ on the complement of the doubly occupied $1s$ determinant. Nonnegative repulsion and the min--max principle therefore leave at most one spectral dimension of $\AtomH{2}{2}$ below $-5/2$. The trial function just computed supplies that dimension. Hence $E$ is simple and the rest of the spectrum lies above $-5/2$. Theorem~\ref{thm:temple} gives the asserted energy interval. The spectral projection of $\psi$ onto this level is nonzero. The symmetries of $\psi$ give the stated choice of $\Phi$. For the sharper gap, let $P_{00}$ project onto that $1s^2$ determinant and $P_{12}$ onto the configurations with one $1s$ and one $n=2$ electron. The normalized $1s$, $2s$, and $2p$ radial factors are proportional to $e^{-2r}$, $(1-r)e^{-r}$, and $re^{-r}$. The identity $\int_0^\infty r^je^{-br}\,dr=j!/b^{j+1}$ gives their mean radii $3/4,3,5/2$. Thus $P_{12}d_{12}P_{12}\leq(15/4)P_{12}$. Weighted Cauchy--Schwarz, followed by the supremum over unit vectors in $\operatorname{ran}P_{12}$, gives $d_{12}^{-1}\geq(4/15)P_{12}$ on the full space. On $P_{00}^\perp$ the nuclear energy is $-5/2$ on $P_{12}$ and at least $-20/9$ on its complement. Thus every form-domain vector $\zeta\perp\operatorname{ran}P_{00}$ satisfies \[ \mathfrak q_{2,2}[\zeta]\geq \min\{-5/2+4/15,-20/9\}\|\zeta\|^2=-\frac{67}{30}\|\zeta\|^2. \] The rank-one min--max comparison now gives $\AtomH{2}{2}|_{\Phi^\perp}\geq-67/30$. Since $-67/30-\mu>67039/100000$, this proves the required gap. \emph{Moments and tails of the exact state.} Put $\beta=-5/2$, $L_0=\mu-\bar v/(\beta-\mu)$, and $\epsilon=(\mu-L_0)/(\beta-L_0)$. The spectral gap at $\beta$ gives, after choosing the phase of $\Phi$, \[ \|\psi-\Phi\|^2\leq2-2\sqrt{1-\epsilon} \leq d_*^2,\qquad d_*=\frac{86434345026}{10^{14}}. \] The last comparison was made rationally as $d_*^2-d_*^4/4\geq\epsilon$, with $d_*<1$. Let $\eta=-2-\mu>0$ and $c_j=(1+\sqrt{1+\eta j^2/2})/\eta$ for $1\leq j\leq8$. Testing the eigenfunction equation with $\min(r_1,T)^{2j}\Phi$ gives, for $X_T=\|\min(r_1,T)^j\Phi\|$, \[ \eta X_T^2\leq 2X_T\|r_1^{j-1}\Phi\|+\frac{j^2}{2}\|r_1^{j-1}\Phi\|^2. \] Here the other electron's one-body energy is at least $-2$ and the repulsion is nonnegative. Induction and monotone convergence give $\|r_1^j\Phi\|\leq c_j\|r_1^{j-1}\Phi\|$ through $j=8$. For $1\leq k\leq4$, set \[ a_k=m_{2k}+d_*\sqrt{m_{4k}},\qquad b_k=d_*\prod_{j=k+1}^{2k}c_j . \] Cauchy--Schwarz applied to the difference of the two moments gives $\|r_1^k\Phi\|^2\leq a_k+b_k\|r_1^k\Phi\|$. All radicals were enclosed by \[ \frac{\operatorname{isqrt}(\lfloor10^{28}x\rfloor)}{10^{14}} \leq\sqrt x< \frac{\operatorname{isqrt}(\lfloor10^{28}x\rfloor)+1}{10^{14}} \quad(x\geq0), \] where $\operatorname{isqrt}(n)=\lfloor\sqrt n\rfloor$ for integers $n\geq0$. Using upper enclosures in $a_k,b_k$, the four positive lower bounds for $M_k^2-a_k-b_kM_k$ were, respectively, \[ \frac{50747334}{10^{14}},\quad \frac{106072203}{10^{14}},\quad \frac{101118508}{10^{14}},\quad \frac{2413688788}{10^{14}}. \] Also $M_k>b_k/2$ in every case, proving the moment bounds. For completeness, the 121 trial-tail calculations used the same polynomial. Integrating $d$ first and splitting at $r_1=r_2$ gives its normalized radial density as $f(r)e^{-gr}+\widetilde f(r)e^{-2gr}$ with rational polynomials $f,\widetilde f$. Each tail integral is evaluated termwise using \[ \int_t^\infty r^je^{-br}\,dr =\frac{j!}{b^{j+1}}e^{-bt} \sum_{h=0}^j\frac{(bt)^h}{h!}. \] To enclose $e^{-x}$, scale $x$ by a power of two into $[0,1]$, use the alternating Taylor polynomial of degree $80$ with remainder bounded by $x^{81}/81!$, and square back with outward rounding to multiples of $10^{-100}$. Signed substitution in the two polynomials produced rational upper bounds $Q_j$ for the trial tails at $j/8$. Every row, $8\leq j\leq128$, satisfies \[ \|\mathbf1_{\{r_1\geq j/8\}}\psi\|^2\leq Q_j,\qquad (\sqrt{Q_j}+d_*)^2\leq P_j,\qquad 0\leq P_j\leq1, \] and all 120 consecutive comparisons give $P_{j+1}\leq P_j$. The root comparisons are integer square comparisons at scale $10^{14}$. The full rational polynomials and endpoint tables are included with the trial function. The triangle inequality transfers these bounds to $\Phi$. Monotonicity of tail probabilities gives the claimed step function for every $t\geq0$, and exchange symmetry gives the assertions for electron two. \end{proof} \subsection{The complementary sectors}\label{sec:13-deferred-proofs-complement} \begin{proof}[Proof of Lemma~\ref{lem:helium-monoanion-complement}] We first remove the sectors without a doubly occupied $1s$ shell. Pair excitation bounds then control every remaining angular pattern with $L\geq2$. \emph{An unfilled $1s$ shell.} Let $h=-\Delta/2-2/r$, with both spin copies, and let $D_2$ project onto the configurations with exactly two $1s$ electrons. Shell $n$ contains the angular momenta $\ell=0,\ldots,n-1$. Indeed, the radial factors $r^\ell e^{-2r/n}L_{n-\ell-1}^{2\ell+1}(4r/n)$, with the associated Laguerre polynomials, satisfy the radial eigen-equation and give $\sum_{\ell=0}^{n-1}(2\ell+1)=n^2$ spatial eigenfunctions. They exhaust the multiplicity in Theorem~\ref{thm:hydrogen}. Within $D_2^\perp$ let $F$ project onto the configurations with one $1s$ and two $n=2$ electrons. By Theorem~\ref{thm:hydrogen}, $\sum_i h_i=-3$ on $F$ and $\sum_i h_i\geq-49/18$ on $D_2^\perp\cap F^\perp$. For $V=\sum_{iE$. \emph{Pair excitation bounds.} For the antisymmetric pair $j,k$, write $H_{jk}=h_j+h_k+d_{jk}^{-1}$ and denote its orbital angular momentum by $J_{jk}$. On $J_{jk}\ne0$, only the $1s\,2p$ configurations lie below $-20/9$ for $h_j+h_k$. Their energy is $-5/2$, and their compressed distance is at most $3/4+5/2=13/4$. The weighted Cauchy--Schwarz argument used above gives a repulsion contribution $4/13>5/18$ on this subspace. Therefore \[ H_{jk}\big|_{\{J_{jk}\ne0\}}\geq-20/9. \] We also need $H_{jk}|_{\{J_{jk}=2\}}\geq\lambda_2$, where $\lambda_2=-2056247529/10^9$. The deficit $(\lambda_2-h_j-h_k)_+$ on this pair sector consists precisely of the $1s\,nd$ configurations for $n=3,4,5$. Indeed their energies are $\epsilon_n=-2(1+n^{-2})$, whereas the next shell has energy $-37/18>\lambda_2$. We now compute the matrix elements of the distance $d_{jk}$ in these configurations, including normalization. At unit charge use the normalized core $2e^{-r}Y_{00}$ and $R_n(r)Y_{20}/\sqrt{S_n}$, with $Y_{00}=(4\pi)^{-1/2}$ and $Y_{20}(\omega)=\sqrt{5/(4\pi)}(3\omega_3^2-1)/2$. Write $R_n(r)=e^{-r/n}\sum_a c_{na}r^a$, with \[ \sum_a c_{3a}r^a=r^2,\quad \sum_a c_{4a}r^a=6r^2-\frac{r^3}{2},\quad \sum_a c_{5a}r^a=21r^2-\frac{14r^3}{5}+\frac{2r^4}{25}. \] The factorial integral gives $(S_3,S_4,S_5)=(98415/8,737280,123046875/8)$ for $S_n=\int_0^\infty r^2R_n(r)^2\,dr$. Define the charge-two orbitals $\phi_{1s}(x)=\sqrt{8/\pi}e^{-2|x|}$ and $\phi_{nd,0}(x)=2^{3/2}R_n(2|x|)Y_{20}(x/|x|)/\sqrt{S_n}$. Their normalization follows from $S_n$, and substitution gives $h\phi_{nd,0}=-2n^{-2}\phi_{nd,0}$. This unitary dilation divides every distance matrix element by two. For $\sigma\in\{-1,1\}$ set $\chi_n^\sigma=(\phi_{1s}\otimes\phi_{nd,0} +\sigma\phi_{nd,0}\otimes\phi_{1s})/\sqrt2$ and put \[ T^\sigma_{nm}=\frac{\delta_{nm}}{\lambda_2-\epsilon_n} -\langle\chi_n^\sigma,d_{jk}\chi_m^\sigma\rangle, \qquad 3\leq n,m\leq5. \] Both exchange signs are needed, paired respectively with triplet and singlet spin. The following formulas specify all six entries for each sign. For nonnegative integers $A,B$ and positive $\alpha,\beta$ define \[ I_{A,B}(\alpha,\beta) =\sum_{h=0}^A\binom Ah \frac{h!(A+B-h)!}{\alpha^{h+1}(\alpha+\beta)^{A+B-h+1}}, \] For $k\in\{2,4\}$, whenever the following subscripts are nonnegative, set $\mathcal M_k(A,B;\alpha,\beta)=I_{A+1-k,B+k}(\alpha,\beta) +I_{B+1-k,A+k}(\beta,\alpha)$. The first expression is the integral of $x^Ay^Be^{-\alpha x-\beta y}$ on $00 . \] All congruences are invertible. Thus $T^+,T^->0$. Rotational invariance makes these distance matrices identical in all five magnetic components. For $\mathcal A=(\lambda_2-h_j-h_k)_+$ on $J_{jk}=2$, conjugating by its positive spectral diagonal gives $\mathcal A^{1/2}d_{jk}\mathcal A^{1/2}\leq I$. Weighted Cauchy--Schwarz implies $d_{jk}^{-1}\geq\mathcal A$, proving the desired pair bound with all spin and magnetic components. \emph{All angular patterns with $L\geq2$.} Set $U=-2903651/10^6$, $g_1=-20/9-U$, and $g_2=\lambda_2-U$. Lemma~\ref{lem:helium-monoanion-neutral} gives $E6779227768$. The case $b=0$ has $\overline d=0$ and requires no division by $b$. These estimates initially hold away from $\rho=0$. The nine-dimensional Hardy inequality $\int\rho^{-2}|u|^2\leq(4/49)\int|\nabla u|^2$ justifies removing a cutoff there. Form continuity removes the outer cutoff and the smoothness restriction. Orthogonal summation proves the second assertion on the closed sum of all $L\geq2$ sectors. \end{proof} \subsection{The exterior estimate}\label{sec:13-deferred-proofs-exterior} \begin{proof}[Proof of Lemma~\ref{lem:helium-monoanion-exterior}] We localize according to which electrons have radii comparable to the largest radius. Call these electrons marked. When exactly one electron is marked, the spectral gap of neutral helium controls the coupling between that electron and the other two. Completing a square in the radial variable of the marked electron then absorbs the localization error and leaves a boundary term. When two or three electrons are marked, the form exceeds $E$ by a positive amount. \emph{Localization and its constants.} Use $\Phi,p_0,M_k$ from Lemma~\ref{lem:helium-monoanion-neutral}, and put \[ R=7,\quad c=\frac{12}{25},\quad a=\frac{99}{100},\quad C=\frac{14629801296936}{10^{12}},\quad K=\frac{1105489614522}{10^{12}}. \] Let $\theta$ be zero on $[0,c]$, equal to $\pi/2$ on $[a,\infty)$, and affine in $\operatorname{arsinh}t$ between $c$ and $a$. For $s=\max_i r_i$ and $A\subset\{1,2,3\}$ define \[ \chi_A=\prod_{i\in A}\sin\theta(r_i/s) \prod_{i\notin A}\cos\theta(r_i/s). \] Then $\sum_A\chi_A^2=1$, and a maximizing label belongs to every nonzero branch $A$. In that branch, $r_i\geq cs$ for $i\in A$ and $r_i\leq as$ for $i\notin A$. Differentiating the product partition, including the derivative of $s$, gives the localization error \[ W=\frac12\sum_A|\nabla\chi_A|^2\leq\frac{C}{s^2}. \] Indeed $|\nabla(r_i/s)|^2=(1+(r_i/s)^2)/s^2$ for each nonmaximizing label, and there are at most two such labels. The finite cutoff calculation uses $h=(a-c)/256$ and \[ t_j=\frac{\operatorname{isqrt} (\lceil10^{24}(1+(c+jh)^2)\rceil)+1}{10^{12}}, \qquad w=h\sum_{j=1}^{256}t_j^{-1}. \] The right endpoint sum gives $\operatorname{arsinh}a-\operatorname{arsinh}c\geq w$. The exact rational comparisons yield \[ \left(\frac{11}{7w}\right)^2\leq C,\qquad \sum_{\ell=4}^{320}\frac{a^{2\ell-8}}{2\ell+1} +\frac{a^{634}}{643(1-a^2)}\leq K. \] The first uses $\pi<22/7$. The second bounds all omitted multipoles by a geometric series. The root inequalities are checked by squaring positive integers, and both sums by clearing positive denominators. On a singleton branch, with marked position $y$ and $r=|y|=s$, the sharper bound is $W\leq C( \mathbf1_{\{r_j\geq cr\}}+ \mathbf1_{\{r_k\geq cr\}})/(2r^2)$. Use the same volume expression for $q_>$ on the localized spinors, which need not be fully antisymmetric. Expanding their gradients gives \[ q_>[u]-E\|u\|^2 =\sum_A\left(q_>[\chi_Au]-E\|\chi_Au\|^2 -\int_{\Omega_7}W|\chi_Au|^2\right). \] \emph{The neutral core in a singleton branch.} At fixed $y$ and spin, the two unmarked electrons remain antisymmetric and their radii are at most $ar$. On their full space define \[ V_y=\sum_{i=1}^2\mathbf1_{\{r_i\leq ar\}} (|y-x_i|^{-1}-r^{-1}),\qquad W_y=\frac{C}{2r^2}\sum_{i=1}^2\mathbf1_{\{r_i\geq cr\}} . \] The radial one-electron marginal of $\Phi$ and the spherical mean of $|y-x|^{-1}$ for $|x| \frac{22968}{100000}. \] Writing a core vector as $\alpha\Phi+v$, $v\perp\Phi$, and completing the square in $\|v\|$ proves \[ \AtomH{2}{2}+V_y-W_y-E\geq-\frac{D(r)}{r^2}I,\qquad D(r)=Cp(r)+\frac{[\mathcal M(r)+C\sqrt{p(r)}]^2}{g(r)r^2}. \] Both $p$ and $\mathcal M$ decrease with $r$, while $g(r)r^2$ increases. Thus $D$ is nonincreasing on $[7,\infty)$. \emph{The radial table and the boundary term.} The exterior table in the code/data release has nodes $\varrho_i=3584/i$, $1\leq i\leq512$. For each node its row selects a rational candidate $\widetilde p_i$ from the five candidates defining $p(\varrho_i)$, hence $\widetilde p_i\geq p(\varrho_i)$. It gives rational upper bounds \[ \mathcal A_i\geq \mathcal M(\varrho_i)+C\sqrt{\widetilde p_i},\qquad \widetilde D_i=C\widetilde p_i+ \frac{\mathcal A_i^2}{g(\varrho_i)\varrho_i^2} \geq D(\varrho_i). \] The two square roots in $\mathcal A_i$ are rounded upward at scale $10^{12}$ by the same integer-square-root rule as above. All 512 rows of the rational sequence $F_0,\ldots,F_{512}$ satisfy \begin{gather*} F_0=0,\qquad F_{i-1}0,\qquad F_{512}=\frac{123555069308}{10^{12}} . \end{gather*} These are the results of integer comparisons after clearing the positive denominators, including $g(\varrho_i)$. The complete selected candidates, upper roots, and $F_i$ are in the exterior table. They imply a bound on every radius, as follows. For $0\leq x\leq1$, interpolate $Y(x)=xf(x)$ linearly through $(i/512,iF_i/512)$ and set $f(x)=Y(x)/x$ for $x>0$. On the $i$th cell, $0\leq f(x)\leq F_i$ and $Y'(x)=iF_i-(i-1)F_{i-1}$. Since $7/x\geq \varrho_i$, \[ Y'(x)-f(x)^2\geq2D(7/x). \] The first cell covers the entire tail $r\geq3584$. For the vector field $\mathcal V(y)=(1-f(7/|y|))y/|y|^2$, expansion of a square on $\Omega=\{y:|y|>7\}$, with outward unit normal $\nu$, gives for $\zeta\in H^1(\Omega)$ \[ \frac12\int_\Omega|\nabla\zeta|^2\geq \frac12\int_\Omega(\operatorname{div}\mathcal V-|\mathcal V|^2)|\zeta|^2 -\frac12\int_{\partial\Omega}\mathcal V\cdot\nu\,|\zeta|^2. \] Apply this to the marked-coordinate slices of the localized spinor. The volume coefficient is $[Y'(x)-f(x)^2]/(2r^2)$, which absorbs the negative term in the lower bound of the preceding step. At $r=7$ the outward normal of the exterior is $-y/7$. Hence the boundary coefficient is \[ \frac{1-F_{512}}{14} =\frac{0.876444930692}{14}>\frac1{16}. \] The vector field is continuous across all cell interfaces, so no internal boundary terms occur. \emph{Two or three marked electrons.} For $k=|A|\in\{2,3\}$ use the marked coordinates $X=(x_i)_{i\in A}$ and $T=|X|^2$. At fixed unmarked coordinates apply the square on $\{X:\max_{i\in A}r_i>R\}$ with vector field $kX/T$. Its volume contribution is $k(k-1)/T\geq(k-1)/s^2$. On an exposed face its boundary contribution is $kR/(2T)\geq1/(2R)=1/14$. For $k=2$ the unmarked electron contributes at least $-2$ by Theorem~\ref{thm:hydrogen}. The triangle bound on each pair distance and minimization over the marked radii give the remaining volume bounds \[ \frac{90372}{100000}-\frac{A_2}{s}-\frac{C-1}{s^2}, \qquad \frac{290372}{100000}-\frac{A_3}{s}-\frac{C-2}{s^2}, \] where \[ A_2=2+\frac2c-\frac1{1+c}-\frac1{1+a}-\frac1{c+a}, \qquad A_3=2+\frac4c-\frac2{1+c}-\frac1{2c}. \] For example, the two-marked potential is bounded below by $s^{-1}[-2-2/t+1/(1+t)+1/(1+a)+1/(t+a)]$, $c\leq t\leq1$. Its derivative is positive. The three-marked expression increases in each of its two radius ratios by the same derivative comparison. Both displayed volume bounds increase with $s\geq7$, and at seven their exact values are \[ \frac{9567964312983109}{947065875000000000}>0,\qquad \frac{1027725017005013}{679875000000000}>0. \] Every branch therefore has nonnegative volume contribution and boundary coefficient at least $1/16$. Fixing the unmarked coordinates introduces no extra boundary: a branch vanishes wherever an unmarked label attains the maximum, and its nonzero traces lie on the exposed faces of $\partial K_7$. Summing the localization identity gives the claim because $\sum_A\chi_A^2=1$ also on those faces. The argument first applies to smooth restrictions. The exterior is a Lipschitz domain, including its corners, so extension, smooth approximation, and continuity of the trace give the free-trace $H^1$ assertion. Coulomb forms pass to this limit by the three-dimensional Hardy inequality in each electron and relative coordinate. No spectral or boundary condition on $u$ is used. \end{proof} \subsection{The upper bound for the lithium anion}\label{sec:13-deferred-proofs-upper} \begin{proof}[Proof of Proposition~\ref{prop:lithium-upper}] \emph{The trial function and its matrix elements.} The trial function is specified by a table of 150 rows of integers in the accompanying code/data release. Its columns are $(c_\alpha,a_{\alpha1},\ldots,a_{\alpha4}, b_{\alpha12},b_{\alpha13},b_{\alpha14},b_{\alpha23}, b_{\alpha24},b_{\alpha34})$, with $1\le\alpha\le150$. The coefficients $c_\alpha$ have no additional scale. Put $D=10^5$. For $x=(x_1,\ldots,x_4)$, let $X_\nu=(x_{1\nu},\ldots,x_{4\nu})^T\in\mathbb R^4$, $1\le\nu\le3$, be the column of $\nu$th Cartesian coordinates of the electron positions. With $e_i$ the coordinate vectors of $\mathbb R^4$, set \[ A_\alpha=\operatorname{diag}(a_{\alpha1},\ldots,a_{\alpha4}) +\sum_{i0$ and $b_{\alpha ij}\ge0$, so $y^TA_\alpha y=\sum_i a_{\alpha i}y_i^2+ \sum_{i0$ for $y\ne0$. Let $P_{ij}$ denote the exchange of the positions $i,j$. Then \[ F=\sum_{\alpha=1}^{150}c_\alpha f_{A_\alpha},\qquad \Phi=(1-P_{12})(1-P_{34})F \] are Schwartz functions. Assign $\Phi/\sqrt6$ to the spin component $\uparrow\uparrow\downarrow\downarrow$ and extend by signed simultaneous permutations to the other five components with two up spins. Set all other components to zero. Since $\Phi$ changes sign under both within-spin transpositions, this defines a fully antisymmetric spinor $\Psi$. The extension is isometric and preserves the Coulomb form. Thus $\Psi$ belongs to the form domain in Set-up~\ref{setup:atoms}. The argument does not require $\Psi$ to be an eigenfunction of the total spin. For $1\le\beta\le\alpha\le150$ and $\sigma\in\{1,(12),(34),(12)(34)\}$, let $B$ be $A_\beta$ with both indices permuted by $\sigma$. The signs of these four permutations are $+,-,-,+$. For each such triple and $v\in\mathbb R^4\setminus\{0\}$, define \[ \begin{gathered} G=A_\alpha+B,\quad g=\det G,\quad \Gamma=\operatorname{adj}G, \quad \tau=\operatorname{tr}(A_\alpha\Gamma B),\quad n(v)=v^T\Gamma v,\\ S=D^6g^{-3/2},\qquad T=\frac{3\tau}{Dg},\qquad J(v)=2\sqrt{\frac{g}{\pi D n(v)}},\qquad \omega=c_\alpha c_\beta(2-\mathbf1_{\alpha=\beta}) \operatorname{sgn}(\sigma). \end{gathered} \] Gaussian integration gives $\langle f_{A_\alpha},f_B\rangle=\pi^6S$. Under the normalized product density, each column $X_\nu$ has covariance $(D/2)G^{-1}$. Differentiating the two Gaussians therefore gives the kinetic quotient $3\operatorname{tr}(A_\alpha G^{-1}B)/D=T$. Radial integration of the Gaussian vector $\sum_i v_ix_i$ gives the Coulomb quotient $J(v)$. Thus, with all sums below over these triples, \[ \mathcal N=\sum\omega S,\qquad \mathcal H=\sum\omega S \left(T-3\sum_iJ(e_i)+\sum_{i\beta$. There are exactly $4\cdot150\cdot151/2=45300$ terms. None is discarded according to its sign or magnitude. \emph{Exact kernel enclosures.} Put $M=2^{120}$ and \[ p_0=\frac{3141592653589793}{10^{15}},\qquad p_1=\frac{3141592653589794}{10^{15}}. \] These enclose $\pi$ strictly. To verify this in rational arithmetic, put $L_k=\sum_{j=0}^{29}(-1)^j/((2j+1)k^{2j+1})$ and $\epsilon_k=1/(61k^{61})$ for $k=5,239$. The tangent addition formula and the alternating-series remainder give \[ p_0<16L_5-4(L_{239}+\epsilon_{239})<\pi <16(L_5+\epsilon_5)-4L_{239}0$ and $n(v)>0$ for the four $v=e_i$ and six $v=e_i-e_j$. Define the integers \[ \begin{aligned} s_{\mathrm l}&=\left\lfloor\sqrt{M^2D^{12}/g^3}\right\rfloor, &s_{\mathrm u}&=s_{\mathrm l}+1,\\ t_{\mathrm l}&=\left\lfloor3\tau M/(Dg)\right\rfloor, &t_{\mathrm u}&=t_{\mathrm l}+1,\\ j_{\mathrm l}(v)&=\left\lfloor\sqrt{4M^2g/(p_1Dn(v))}\right\rfloor, &j_{\mathrm u}(v)&=\left\lfloor\sqrt{4M^2g/(p_0Dn(v))}\right\rfloor+1,\\ k_{\mathrm l}&=t_{\mathrm l}-3\sum_i j_{\mathrm u}(e_i) +\sum_{i0,\qquad H_+<0,\\ \left\lfloor\frac{10^9H_-}{MN_-}\right\rfloor=-7497020241, \qquad \left\lceil\frac{10^9H_+}{MN_+}\right\rceil=-7497020240. \end{gathered} \end{equation} The input, executable checker and complete execution record are supplied with the table in the accompanying code/data release. The checker reads every eleven-integer row, checks the row signs, and visits every lower-triangular pair and all four permutations. Its cofactor expansion computes $\Gamma$ and $g$ exactly. Its kinetic sum is $3\sum_{i,j,k}(A_\alpha)_{ij}\Gamma_{jk}B_{ki}=3\tau$. Nuclear and pair cofactor forms are respectively $\Gamma_{ii}$ and $\Gamma_{ii}+\Gamma_{jj}-2\Gamma_{ij}$, so its kernel is precisely the one just proved. The execution uses Python integers, rational arithmetic, signed floor division and integer square roots, with assertions enabled. Faithful input reading, execution and output recording have the meaning of Set-up~\ref{setup:execution}. No floating-point accuracy assumption enters this evaluation. Since $N_->0$, some $c_\alpha\ne0$. The identity-permutation diagonal term then has positive weight $c_\alpha^2$ and strict overlap upper bound $MS