\section{Helium quadratic-weight certificates}\label{sec:12-helium-quadratic-certificates}

This appendix proves the two computer-assisted inputs of
Section~\ref{sec:04-helium-dianion}. The first is the pointwise lower
bound for the weighted repulsion (Lemma~\ref{lem:he4-quadratic-screen}).
The second is the pair of eigenvalue counts for the one-electron operator
(Lemma~\ref{lem:he4-quadratic-levels}). The conventions are those of
Appendix~\ref{sec:09-geometric-certificates}. Every accepted inequality is
evaluated in exact rational arithmetic. Floating-point arithmetic is used
only to propose auxiliary vectors and knot values. In this appendix,
Set-up~\ref{setup:execution} means faithful Python integer and rational
operations, file operations and execution records, with assertions
enabled. The accompanying code/data release contains the saved
certificates, their exact readers and the completed execution records.

\begin{definition}[Helium quadratic-weight data]\label{def:he4-quadratic-data}
Let $g$ be the continuous function on $[0,\infty)$ that is affine between
the knots
\[
 \begin{array}{c|ccccc}
 r & 1/10 & 2/5 & 3/2 & 5 & 20\\ \hline
 g(r) & 41/10 & 33/10 & 1/2 & -1/10 & 3
 \end{array}
\]
and constant on $[0,1/10]$ and on $[20,\infty)$, and put $f(r)=2r+g(r)$.
With $(b_a,\delta_a)$ from \eqref{eq:helium-dianion-cap},
$\lambda_1=22/25$, $\lambda_2=19/100$, and
$B_a(s)=(s-b_a)_+^2-\min\{s/b_a,1\}/(2\delta_a)$ as in
Proposition~\ref{prop:quadratic-removal}, define for
$x=(x_1,\ldots,x_4)\in(\mathbb R^3)^4$ with pairwise distinct positions
\[
 D(x)=\sum_{i=1}^4f(r_i)-\sum_{i<j}\frac{r_i^2+r_j^2+2}{d_{ij}}
 -\lambda_1B_1(q_1)-\lambda_2B_2(q_2),
\]
where $q_1\le q_2$ are the two smallest radii.
\end{definition}

\subsection{The four-electron quadratic screen}

\begin{lemma}[Four-electron quadratic screen]\label{lem:he4-quadratic-screen}
Assume Set-up~\ref{setup:execution} for the specified He4 quadratic
certificate execution. Then $D(x)\le1$ for every
$x\in(\mathbb R^3)^4$ with pairwise distinct positions.
\end{lemma}

The floating-point supremum of $D$ is about $0.786$, attained near the
radii $(2.70,5.43,7.66,7.66)$ with the two largest electrons antipodal.
The certification uses the slack $0.21$ between this value and the bound.
The constant $1$ enters the proof of Theorem~\ref{thm:helium-dianion} as
the term $-\|u\|^2$.

\begin{proof}
$D$ is invariant under permutations of the electrons, so it suffices to
consider ordered radii $r_1\le r_2\le r_3\le r_4$, where $q_a=r_a$. The
certificate covers the ordered radius space $\{0\le r_1\le\cdots\le r_4\}$
by boxes $\prod_i[x_i,y_i]$, with $x_i\le y_i$ nondecreasing in $i$ and
$y_i=\infty$ permitted, and proves $D\le1$ on each box by an explicit
upper bound $\mathcal U(\mathrm{box})$ computed in rational arithmetic.
A box with $\mathcal U>1$ is bisected by a fixed deterministic rule.
Normally the box is cut at
the midpoint of the bounded coordinate $i$ maximizing the relative width
$(y_i-x_i)/(x_i+\frac3{10})$. When every bounded relative width is
below $\frac1{20}$, its first unbounded coordinate is cut instead, at
$\max\{2x_i,x_i+1\}$. The children are intersected with the ordered cone.
This continues until every leaf is accepted. The root boxes are the $4845$
nondecreasing index tuples of the radial partition
$0,\frac1{10},\frac25,1,\frac32,2,3,4,5,8,12,20,40,80,160,320,640,\infty$.
Hence no coordinate interval of any box contains a knot of $g$ or one of
$b_1,b_2$ in its interior. Consequently $f$ is affine and $B_a$ is
quadratic on each coordinate interval.

\emph{Bounded boxes.} Four elementary estimates give $\mathcal U$.
\begin{enumerate}
\item \emph{Angle elimination.} For $b,K>0$ and $d>0$,
 $b/d\ge\frac32b^{2/3}K^{1/3}-\frac12Kd^2$ (the arithmetic--geometric
 mean inequality for $b/(2d),b/(2d),Kd^2/2$). For a positive semidefinite
 $4\times4$ matrix $K$ with nonnegative entries,
 $\sum_{i<j}K_{ij}d_{ij}^2\le\sum_ir_i^2(K\mathbf 1)_i$, because the
 difference equals $-\sum_{i,j}K_{ij}\,x_i\cdot x_j\le0$. The certificate
 uses $K=vv^{\mathsf T}+uu^{\mathsf T}$ with $v,u\in\mathbb Q_+^4$ proposed
 by a floating-point optimizer and recorded, on a recorded subset $S$ of
 the bounded coordinates. The choice affects the tightness of
 $\mathcal U$ and not its validity. Hence, on the box and for pairs in $S$,
 \[
  \sum_{i<j}\frac{r_i^2+r_j^2+2}{d_{ij}}
  \ge\sum_{i<j}\tfrac32\,\psi(r_i,r_j)\,K_{ij}^{1/3}
  -\tfrac12\sum_ir_i^2(K\mathbf 1)_i,\qquad
  \psi(r_i,r_j)=(r_i^2+r_j^2+2)^{2/3}.
 \]
\item \emph{Convexity and roots.} The function $\psi$ is jointly convex,
 because its Hessian is
 $\frac43(2+s)^{-4/3}[(2+s)I-\frac23\,rr^{\mathsf T}]\succeq0$ with
 $s=r_i^2+r_j^2$. Hence on the box $\psi$ is bounded below by its tangent
 plane at the box centre. The value and gradient of this plane are
 enclosed by rational bounds. Every cube root is replaced by a rational
 bound of the correct direction, certified by an integer power comparison.
\item \emph{Moments.} $B_a$ is convex, so it is bounded below by its
 tangent at the box centre, and $-\lambda_aB_a(r_a)$ by an affine
 function of $r_a$.
\item \emph{Vertex maximization.} After 1--3, $D$ is bounded on the box
 by a sum of affine functions of the $r_i$ and the convex term
 $\frac12\sum_ir_i^2(K\mathbf1)_i$. The maximum of this bound over the box
 is attained at one of the sixteen vertices, where it is evaluated exactly.
\end{enumerate}

\emph{Unbounded boxes.} For a pair with an unbounded radius the pair term
is bounded instead by the elementary inequalities
$(r_i^2+r_j^2)/d_{ij}\ge\max\{|r_i-r_j|,(r_i+r_j)/2\}$, which follow from
$d_{ij}\le r_i+r_j$ and $r_i^2+r_j^2\ge|r_i^2-r_j^2|$, together with
$2/d_{ij}\ge2/(y_i+y_j)$ on bounded pairs and $0$ otherwise. These make
$\mathcal U$ an affine function of each unbounded radius. Its slope is
nonpositive in $r_3$ and $r_4$, because each such electron receives at
least $\frac32r_i$ from its pairs against $2r_i$ from $f$ only when all
four radii are large, and that configuration is where the moment terms
act. For $r_1$ and $r_2$ the remaining positive slope is absorbed by the
concave quadratic $-\lambda_a(r_a-b_a)^2$, whose maximum over the ray is
explicit. The same elementary bounds are used for bounded pairs not
contained in $S$, where $|r_j-r_i|$ is taken when the centre radii satisfy
$r_j\ge3r_i$ and $(r_i+r_j)/2$ otherwise, together with
$2/d_{ij}\ge2/(y_i+y_j)$. The certificate records $S$ for each accepted
box.

\emph{Coverage and execution.} The children of a box are two boxes whose
union is the box intersected with the ordered cone, so the accepted leaves
cover the ordered radius space. Since $D$ is symmetric, they cover
$(\mathbb R^3)^4$ minus the collision sets. The execution
(\texttt{certify\_screen\_dump.py} with the data of
Definition~\ref{def:he4-quadratic-data} and target $1$) terminated after
evaluating 69{,}119 boxes, of which 36{,}982 were accepted and the rest
bisected. The maximal depth was 15 and the smallest accepted slack was
$1-\mathcal U=1.483\cdot10^{-4}$. The run took 4.0 hours on one core, and
no box failed.
The log of evaluated boxes, with the recorded $S$ and $(v,u)$ of each
accepted box, is re-read by the exact reader
(\texttt{replay\_screen.py}). The reader rebuilds the bisection tree from
the root boxes with the rule above, recomputes every $\mathcal U$ in
rational arithmetic and confirms that every leaf is accepted. It uses no
optimizer.
\end{proof}

\begin{remark}[Controls]\label{rem:he4-quadratic-controls}
Two checks were run that are not part of the proof. (a) Asked to certify
the target $\frac{7}{10}$, which lies below the numerical supremum
$0.786$, the same program fails, reporting the box
$(2.8139,5.7598,8.8755,9.0018)^{\pm10^{-4}}$ with $\mathcal U=0.70007$, next to the true maximizer. (b) A
randomized test compared $\mathcal U$ with angle-optimized sampled values
of $D$ on $300$ random ordered boxes and found no violation.
\end{remark}

\subsection{The helium radial indices}

\begin{lemma}[Helium radial indices]\label{lem:he4-quadratic-levels}
Let $h$ be the operator of \eqref{eq:helium-dianion-onebody}. With spin
excluded from the strictly negative form index,
\[
 \NegIndex\Bigl(h+\frac{197}{100}\Bigr)=0,\qquad
 \NegIndex\Bigl(h+\frac3{25}\Bigr)\le1 .
\]
(Floating-point values, not used in the proof: the two lowest $s$-levels
of $h$ are $-1.948$ and $-0.095$, and the lowest $p$-level is $0.451$.)
\end{lemma}

\begin{proof}
\emph{Reduction to radial forms.} Put $a(r)=2+r^2$ and, for a real level
$\tau$,
\[
 V_\tau(r)=-\frac2r+\frac{2r+g(r)-\tau}{2+r^2}-\frac{r^2}{2(2+r^2)^2}.
\]
For $\varphi$ in the form domain of $h$, the function
$\psi=a^{1/2}\varphi$ lies in $H^1(\mathbb R^3)$, since
$|\nabla a^{1/2}|^2=r^2/(2+r^2)\le1$, and integration by parts on
compactly supported functions followed by density gives
\[
 q_h[\varphi]-\tau\|\varphi\|^2
 =\int_{\mathbb R^3}\Bigl(\frac12|\nabla\psi|^2+V_\tau|\psi|^2\Bigr)dx ,
\]
the term $-\frac32$ of $h$ being exactly the term
$-\frac12a^{1/2}\Delta a^{1/2}+\frac12|\nabla a^{1/2}|^2=-\frac32+\frac{r^2}{2(2+r^2)}$
produced by the substitution, up to the displayed last term of $V_\tau$.
The map $\varphi\mapsto a^{1/2}\varphi$ is injective, so
$\NegIndex(h-\tau)\le\NegIndex(-\frac12\Delta+V_\tau)
=\sum_{\ell\ge0}(2\ell+1)\,\NegIndex(q_{\ell,\tau})$, where
\[
 q_{\ell,\tau}[u]=\int_0^\infty\Bigl(\frac12|u'|^2
 +\Bigl(V_\tau+\frac{\ell(\ell+1)}{2r^2}\Bigr)|u|^2\Bigr)dr
\]
on $H^1_0((0,\infty))$. Since $q_{\ell,\tau}$ increases with $\ell$ and
with $-\tau$, it suffices to prove
\[
 \NegIndex(q_{1,\tau_1})=0,\qquad \NegIndex(q_{0,\tau_1})\le1,\qquad
 \NegIndex(q_{0,\tau_0})=0,\qquad \tau_0=-\frac{197}{100},\ \tau_1=-\frac3{25}.
\]

\emph{Supersolution criterion.} Let $W=V_\tau+\ell(\ell+1)/(2r^2)$ and let
$y$ be locally Lipschitz on an open interval $J\subset(0,\infty)$ with
\begin{equation}\label{eq:he4-quadratic-riccati}
 y'+y^2\le2W\quad\text{on }J .
\end{equation}
For $u\in C_c^\infty(J)$, integrating
$-\operatorname{Re}(\bar u'u)\,y=-\frac12(|u|^2)'y$ by parts gives
\[
 \int_J\Bigl(\frac12|u'|^2+W|u|^2\Bigr)
 =\int_J\frac12|u'-yu|^2+\int_J\Bigl(W-\frac12(y'+y^2)\Bigr)|u|^2\ge0 ,
\]
and by density $q_{\ell,\tau}\ge0$ on all form-domain functions vanishing
at the finite endpoints of $J$. With $J=(0,\infty)$ the index is $0$. With
$J=(0,c)$ and $J=(c,\infty)$ it is at most $1$, because one Dirichlet
condition has been imposed.

\emph{The certificates.} Take
\[
 y=\frac{\ell+1}{r}+\frac{k}{r-c}+z(r),\qquad k\in\{0,1\},
\]
with $z$ piecewise affine with rational knots $0=r_0<\cdots<r_N=40$ and
$z=\alpha/r$ on $[40,\infty)$, $\alpha\in\mathbb Q$. The values
$z(0)=-2/(\ell+1)$ for $k=0$, $z(0)=1/c-2$ for $k=1$, and $z(c)=-1/c$
cancel the Coulomb pole at the origin and the pole at the cut
identically. The knots of $g$ are among the $r_j$, so $g$ is affine on
each knot interval. The expression $y'+y^2-\ell(\ell+1)/r^2$ equals
$z'+2(\ell+1)z/r+z^2$ for $k=0$ and $z'+z^2+2z/r+2(1+rz)/(r(r-c))$ for
$k=1$, $\ell=0$. Multiplying \eqref{eq:he4-quadratic-riccati} by
$r(2+r^2)^2|r-c|^k$ therefore turns it, on each knot interval, into a
polynomial inequality
$Q(r)\ge0$ of degree at most eight with rational coefficients. Each is
certified by nonnegativity of its Bernstein coefficients after bisection.
The same method is used on $[40,400]$. On $[400,\infty)$ the inequality is
certified by nonnegativity of all Taylor coefficients at $400$. The three
certificates are:
\begin{itemize}
\item[(A)] $\ell=1$, $\tau=\tau_1$, $k=0$, $\alpha=1$: $76$ pieces;
 gives $\NegIndex(q_{\ell,\tau_1})=0$ for all $\ell\ge1$.
\item[(B)] $\ell=0$, $\tau=\tau_1$, $k=1$, $c=75450851/50000000$,
 $\alpha=23/100$: $502$ pieces; gives $\NegIndex(q_{0,\tau_1})\le1$.
\item[(C)] $\ell=0$, $\tau=\tau_0$, $k=0$, $\alpha=2$: $617$ pieces;
 gives $\NegIndex(q_{\ell,\tau_0})=0$ for all $\ell\ge0$.
\end{itemize}
The knot values $z(r_j)$ were proposed by a floating-point integration of
the regular solution of $h$ at the raised levels $\tau+\varepsilon$
($\varepsilon=0.15,0.012,0.011$), and were rounded to multiples of
$10^{-9}$. The Riccati residual $2\varepsilon/(2+r^2)$ of this solution is
the slack that the piecewise affine interpolation uses. The proposal is
not part of the proof. The certificate is the list of knots and values
(\texttt{levels\_super\_certificate.json}, $1195$ polynomial
inequalities). It is generated by \texttt{certify\_levels\_super.py} and
re-checked in exact arithmetic by \texttt{replay\_levels\_super.py} in a
few seconds. The reader rejects the certificate when a single knot value
of (B) is raised by $1/50$.
\end{proof}

\begin{remark}[Cross-check]
The same four index counts $(0,0,1,0)$, for $(\ell,\tau)$ equal to
$(0,\tau_0)$, $(1,\tau_0)$, $(0,\tau_1)$ and $(1,\tau_1)$, were first
obtained by the cell lower-form method of
Appendix~\ref{sec:09-geometric-certificates}
(\texttt{certify\_levels.py}). That computation uses $24{,}005$ cells from
$r_0=1/256$ to $40$,
cellwise constant lower bounds on $V_\tau$, the Dirichlet--Poincar\'e
constant $4.9<\pi^2/2$, and exact pivot counting of the assembled
tridiagonal matrix in outward-rounded interval arithmetic. The two
methods agree. The levels $\tau_0,\tau_1$ leave room: the floating-point
ground level of $h$ is $0.022$ above $\tau_0$, and its first excited
$s$-level is $0.025$ above $\tau_1$.
\end{remark}