\section{Setting and conventions}\label{sec:02-setting}

This section fixes the model and the notation, and it states the assumptions
under which the computer-assisted statements hold.

\begin{setup}\label{setup:atoms}
We use Hartree atomic units, an infinitely heavy point nucleus, and electrons
of spin $1/2$. Write $\mathbb N=\{1,2,\ldots\}$. For an integer $N\geq1$, let
\[
 \FermionSpace{N}=\bigwedge^N L^2(\mathbb R^3;\mathbb C^2).
\]
For $Z>0$, the operator $\AtomH{N}{Z}$ is associated with the closed Coulomb
form
\[
 \mathfrak q_{N,Z}[u]=\frac12\sum_{i=1}^N\int|\nabla_i u|^2
 -Z\sum_{i=1}^N\int\frac{|u|^2}{|x_i|}
 +\sum_{i<j}\int\frac{|u|^2}{|x_i-x_j|}
\]
on $H^1((\mathbb R^3)^N;(\mathbb C^2)^{\otimes N})\cap\FermionSpace{N}$.
All integrals include the sum over spin components. Antisymmetry exchanges
positions and spins simultaneously. Write
\[
 \AtomE{N}{Z}=\inf\sigma(\AtomH{N}{Z}),\qquad \AtomE{0}{Z}=0,
 \qquad
 \AtomCount{Z}=\sup\{N\in\mathbb N:\AtomE{N}{Z}<\AtomE{N-1}{Z}\}.
\]
We say that $N$ electrons are strictly bound if
$\AtomE{N}{Z}<\AtomE{N-1}{Z}$. The absence of eigenfunctions at the
threshold $\AtomE{N-1}{Z}$ is a separate assertion. No restriction on total
spin, angular momentum, parity or magnetic quantum number is imposed unless
explicitly stated. For configurations we write $r_i=|x_i|$,
$d_{ij}=|x_i-x_j|$, and $q_1\leq\cdots\leq q_N$ for the ordered radii.
All displayed terminating decimal bounds denote exact rational numbers.
We write $s_+=\max\{s,0\}$ for $s\in\mathbb R$ and $I$ for the identity
on the Hilbert space under consideration.
For a semibounded quadratic form $q$, $\NegIndex(q)$ is the supremum of the
dimensions of subspaces on which $q$ is strictly negative away from zero.
\end{setup}

\begin{setup}\label{setup:execution}
The computer-assisted statements use the fixed inputs and executable
algorithms specified in the mathematical appendices and accompanying code/data
release. Exact arithmetic, decoding, file operations and recorded executions
are assumed faithful. Where binary floating-point arithmetic is used, the
specified source, operation order, precision, rounding, underflow, dispatch,
thread and interface conditions are part of the execution assumptions.
The appendices state those conditions for each affected calculation and prove
the numerical error bounds. Accuracy, complete coverage and physical
normalization are conclusions of the checks and proofs, not runtime assumptions.
\end{setup}