\section{Computations}\label{app:computations}

\subsection{List of computational statements}\label{app:list}

\Cref{tab:computations} lists the statements that rest on, or were checked by, machine computation.  All arithmetic is exact: integers, rationals, polynomials, number fields given by defining polynomials, and finite fields.  The one exception is the enclosure of the number $R$ in \cref{app:classnumber}, which uses ball arithmetic: floating-point intervals that are guaranteed to contain the exact values.  The only class group that the proof uses is that of $\Lt$, determined in \cref{app:classnumber} by an argument that uses no unproved hypothesis.\looseness=-1

\begin{table}[ht]
\centering
\footnotesize
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.27\linewidth}>{\raggedright\arraybackslash}p{0.69\linewidth}@{}}
\toprule
Statement & What is computed \\
\midrule
\cref{lem:disc}, \eqref{eq:belyi}, \eqref{eq:bnorms} & polynomial identities, discriminants and resultants \\\addlinespace[2pt]
\cref{lem:fields,lem:labels} & maximal orders of $\Lo$ and $\Lt$ (\texttt{nfinit}, certified by \texttt{nfcertify}), signatures, discriminants, prime decompositions (\texttt{idealprimedec}), labels \\\addlinespace[2pt]
\cref{lem:psi5} & checked by \texttt{factorpadic} (the proof is by hand) \\\addlinespace[2pt]
\cref{prop:A3} & the types of $\Lo$ at the primes $q\equiv1\pmod5$ up to $700$ and the types of the forms of \cref{prop:A1}; the admissible residues, families and the sets $\Iq$ \\\addlinespace[2pt]
\cref{prop:basis}(i), \cref{lem:normdata} & characteristic polynomials and ideal factorizations of the $B_j$; the valuation matrix; the symbol matrices and their ranks; the exact norm identities \\\addlinespace[2pt]
\cref{thm:sieve} & the linear algebra over $\F_5$ and the exhaustive enumeration of the $5^{10}$ vectors of $\mathcal A$ \\\addlinespace[2pt]
\cref{rem:robust,rem:whyfive}, \cref{sec:control} & further runs of the sieve, and the ranks of the maps $c\mapsto\Mq c$ on $\mathcal A$; the tests on the fibres above $\eta=-1$ and $\eta=243$ \\\addlinespace[2pt]
\cref{thm:classnumber} (\cref{app:classnumber}) & the prime ideals of $\Lt$ of norm at most $10^7$ (two methods); an enclosure of $R$ in ball arithmetic; for each of these prime ideals, a generator, checked by exact arithmetic; the corresponding computations for $\Lo$ (\cref{rem:classnumberL8}) \\
\bottomrule
\end{tabular}
\vspace{3pt}
\caption{The computational statements of the paper.}\label{tab:computations}
\end{table}

The computations for \cref{lem:fields,lem:labels,prop:A3,prop:basis,lem:normdata,thm:sieve} take a few minutes in total on one core of a laptop, most of it in the exhaustive sieve.  The tests of \cref{sec:control} take a few minutes each.  The computations of \cref{app:classnumber} take about an hour and a quarter: a few minutes for each list of prime ideals and for the enclosure of $R$, and about an hour for the generators of the $665\,770$ prime ideals.

We describe how the data of \cref{app:data} are obtained and checked.  The field $\Lt$ is built as $\Lo[x]/(x^3+20x^2+350x+8750)$, where the cubic is the minimal polynomial of $25b$, and represented by an absolute defining polynomial of degree $24$.  The elements $a$ and $b$ are expressed in this absolute representation, and the printed elements $B_j$ and $u_i$, given as polynomials in $a$ and $b$, are evaluated there.  The candidates $B_j$ were found with PARI's \texttt{bnfinit} and \texttt{bnfunits}.  This uses the generalized Riemann hypothesis, but only to find the elements, whose properties are then checked unconditionally: the $S$-unit property by characteristic polynomials and by ideal factorization, the valuations by \texttt{nfeltval}, and the independence by the rank of the symbol matrix.  For the auxiliary primes, the residue fields $k(\qq)$ and $k(\qQ)$ are handled with \texttt{nfmodpr}.  The roots of $f_{\bar\eta}$ in $k(\qq)$ are found with \texttt{polrootsmod} and transported to $k(\qQ)$ by lifting to $\Lo$, embedding in $\Lt$ and reducing.  A separate program recomputes every row of every matrix $\Mq$ from the description of the primes in \cref{tab:primesq} alone, by arithmetic in finite fields (\texttt{ffgen}, \texttt{ffextend}), and finds the same $97$ rows.

\subsection{Independent second computations}\label{app:independent}

The following computations were repeated by separately written programs, which share with the first ones only the definitions in the text and, where stated, the printed data and the defining polynomial of $\Lt$.
\begin{itemize}[leftmargin=2em]
\item \emph{The auxiliary primes and the sets $\Iq$} (\cref{prop:A3}), in Python with FLINT and explicitly constructed finite fields: the same set $\cQ$, the same entries of \cref{tab:aux} and the same sets $\Iq$.  This program also checked that every vector of every $\Iq$ satisfies the relation between the symbols above a prime $\qq$ of $\Lo$ and the symbol of $2$ at $\qq$ that \cref{prop:D2} implies.
\item \emph{The sieve} (\cref{thm:sieve}) \emph{and the tests of \cref{sec:control}}, with an independent model of $\Lt$, its own basis of $S$-units, the norm condition imposed through valuations and residue symbols in $\Lo$, and its own labels and sets $\Iq$: the same dimensions $14$ and $10$, the same counts $36\,875$, $567$, $19$, $1$, $0$, and the same single survivor in both test fields.  It also agrees with the printed valuation matrix, norm identities, matrices $\Mq$ and sets $\Iq$.\looseness=-1
\item \emph{The class number of $\Lt$} (\cref{app:classnumber}).  Two programs, both starting from the same defining polynomial of $\Lt$ as the first ones, list the prime ideals of norm at most $10^7$, by the Dedekind--Kummer theorem for the primes not dividing its index and, for the few others, by \texttt{idealprimedec} or a second defining polynomial, and find the same $665\,770$ prime ideals.  Each encloses $R$ with its own closed form for $g$ and its own treatment of the integral, and both obtain $R=0.62954313841571501\ldots$, with radii less than $2.5\cdot10^{-21}$ and $3.3\cdot10^{-19}$.  A further program proves again that all $665\,770$ prime ideals are principal, with another defining polynomial of $\Lt$ and its own certified maximal order.
\end{itemize}

\subsection{Software}\label{app:software}

The computations used PARI/GP 2.17.3~\cite{PARI}, Python 3.12 with NumPy, SciPy, SymPy and mpmath, and FLINT 3.3~\cite{FLINT} through python-flint 0.8, including the ball arithmetic of Arb~\cite{Arb} for \cref{app:classnumber}.

\subsection{Data availability}\label{app:data-availability}

The inputs, programs and outputs of all computations, with scripts that run them in order and a document that describes them, are deposited at~\cite{Companion257}.  The Lean formalization of \cref{thm:L8,thm:main} described in \cref{sec:assumed} is deposited at~\cite{Lean257}.

\section*{Declarations}

\subsection*{Research methodology}
The author designed and operated the multi-agent research system used in this work, built on Anthropic Claude Opus~5.5.  The system carried out literature analysis, mathematical development and computation, with checks assigned to agents separate from those developing the arguments.

\subsection*{Funding}
This research did not receive any specific grant from funding agencies in the public, commercial, or not-for-profit sectors.

\subsection*{Declaration of competing interests}
The author declares no competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

\subsection*{Declaration of generative AI and AI-assisted technologies in the manuscript preparation process}
Anthropic Claude Opus~5.5 was used to draft and revise the manuscript.  The author reviewed the material and takes full responsibility for the article.