\section{Verification}\label{sec:verification}

The proof of Theorem~\ref{thm:main} consists of the arguments in the text and the computations they invoke, classified in \S\ref{ss:checks}. It does not use the cross-checks of \S\ref{ss:crosschecks} or Remarks~\ref{rem:P1hand} and~\ref{rem:AB}, nor any re-check these arguments do not invoke. The certificates, the programs that check them, their logs and the supplementary notes are in the supplementary material, with a checksum for each file. It is available at \url{https://doi.org/10.5281/zenodo.23202861}.

Some objects have other names in the supplementary material. The points $\hone$, $\htwo$ and $\hthree$ (Tables~\ref{tab:points} and~\ref{tab:noK}) are \texttt{X52}, \texttt{X29} and $48_1$ there, and the points of Table~\ref{tab:points} appear under the point records in its last column. The relations (R1), (R2) and (R3) of \S\ref{ss:d5} are called gen, det and tilde there and are proved as Theorems G, D and T of its module \texttt{d5fam}; the model of the centred case (\S\ref{ss:d5}) is that of its Theorem~C0. Theorem~\ref{thm:gate} is Theorem G of its module \texttt{nod2route}. Theorem~\ref{thm:S} is Theorem S of its module \texttt{strata}, in which $\mathbf q_*$ and $\mathbf p_*$ are zeros of the flats \texttt{F89} of the face $1|2|3|4|5$ and \texttt{F49} of the face $1|2|3|45$. The points $\mathbf q_*$ and $\mathbf p_*$ also appear under the point records $52_0$ and $47_0$. The jump points of $T_9$ (Proposition~\ref{prop:farT9}) fall there into numbered classes: the point $s=\rho_0/4$ is class $11$, and the two points $s\approx0.0520549$ and $s\approx0.176101$ form class $14$. The table of re-checks is the file \texttt{CHECKS.md}.

\subsection{Literature}\label{ss:literature}
We list the inputs from \cite{AK12} in \S\ref{ss:akinputs}.

\subsection{Classes of computations}\label{ss:checks}
\begin{enumerate}[label=(\arabic*)]
\item \emph{Exact rational arithmetic.} The lexicographic certificates (\S\ref{sec:lex}) are lists of integer functionals. We recompute the attained faces of the pieces in rational arithmetic and check every inequality in integers. The checks take the hulls of \S\ref{ss:d5} from files. We verify in exact arithmetic that each polytope in these files is the polytope of Table~\ref{tab:d5hulls} for its pair of modes, or its image under Lemma~\ref{lem:d5sym}. We make the exact algebraic decisions of class (C2) (\S\ref{ss:masscert}) in exact arithmetic over $\Q$ and over number fields $\Q[\theta]/(f)$.
\item \emph{Ball arithmetic.} We show that polynomials, such as those of labels, do not vanish at exact mass points, and we isolate real roots. We certify isolated zeros of polynomial systems by Krawczyk's test \cite{Kra69,Moo77,Neu90}. We use Arb in FLINT 3.6.0, through python-flint 0.9.0.
\item \emph{Standard bases.} We prove that a polynomial system has no solution by a standard basis over $\Q$ or $\Q(\jj)$ (Singular 4.4.1), or modulo large primes together with a lifting argument (\S\ref{sec:points}). In Theorem~\ref{thm:typeII} we bound the number of solutions of a system by a standard basis over $\Q$. In \S\ref{sec:strata}, by standard bases, minimal primes and saturations over $\Q$, we describe the points of the strata at which given labels hold. We use msolve to search for solutions, version 0.9.4 for every run whose output enters a proof. Where its output enters a proof we verify it: we check the rational parametrizations against the input polynomials and prove their completeness separately.
\item \emph{The special rays.} We obtain the counts of \S\ref{sec:rays} from a branch and bound in double precision with outward rounding.
\end{enumerate}
We verify each lexicographic certificate of the paper with a program different from the one that found it. The \emph{independent checker} of lexicographic certificates is a program written from the definitions and the tables of this paper; it shares no code with the search programs. It re-verifies in particular the certificates of the label sets in the proof of Theorem~\ref{thm:S} and the two certificates of Proposition~\ref{prop:Spoints}(c). The re-checks, with their counts, are tabulated in the supplementary material. They cover the computations of the proof except those in Table~\ref{tab:notrechecked}.

\begin{table}[ht]
\centering
\small
\begin{tabular}{@{}p{0.36\textwidth}p{0.58\textwidth}@{}}
\toprule
computation & not re-checked\tabularnewline
\midrule
\raggedright the flats of the computation (Proposition~\ref{prop:Stree}) & \raggedright a second enumeration of the flats from scratch\tabularnewline[2pt]
\raggedright the conditions on the primes, where (P1) is re-checked for the runs of Theorem~\ref{thm:KA} & \raggedright the other conditions, which are checked within the runs\tabularnewline[2pt]
\raggedright the searches of Proposition~\ref{prop:raycount} and Theorem~\ref{thm:countP1} & \raggedright the upper bounds, which rest on the exclusion tests and on the outward rounding of the search\tabularnewline
\bottomrule
\end{tabular}
\caption{Parts of the computations of the proof that the re-checks leave out.}\label{tab:notrechecked}
\end{table}

The following results rest also on computations stated in full in their proofs: Proposition~\ref{prop:eqfull}, Theorems~\ref{thm:W}, \ref{thm:typeII} and~\ref{thm:col}, Lemma~\ref{lem:Pdata}, Theorems~\ref{thm:points} and~\ref{thm:gate}, Propositions~\ref{prop:Stree}, \ref{prop:Spoints} and~\ref{prop:farT9}, Theorem~\ref{thm:SJ}, Lemma~\ref{lem:K14FAFB}, Proposition~\ref{prop:d14a}, Theorem~\ref{thm:RL}, and Theorems~\ref{thm:count1}, \ref{thm:count2} and~\ref{thm:countP1}. For the following results we list the computations here.
\begin{itemize}
\item The relations (R1)--(R3) of \S\ref{ss:d5}: an elimination whose generator has only positive coefficients for (R1), $36$ eliminations by standard bases over $\Q$ for (R2), and a polynomial identity for (R3).
\item Proposition~\ref{prop:d6P2}: the checks (i)--(iv) of its proof, made as stated there in exact arithmetic, by a standard basis over $\Q$ and in ball arithmetic.
\item Proposition~\ref{prop:d3tstar}: the checks (i)--(iii) of its proof, by exact rational bisection and in ball arithmetic.
\end{itemize}

We apply the certificates that use the hull $\VN$ of \S\ref{ss:d5} only at points where $\VN$ is valid. Eleven of the certificates in the proof of Proposition~\ref{prop:exceptional}, used at ten jump points of $T_1$, $T_4$ and $T_5$ and at ten jump points of $T_8$, are relative to $\VN$. All others there are relative to $\Vtwo^{\mathrm w}$. At these jump points, at the two point records of Table~\ref{tab:points} whose final checks use $\VN$, and at $\mathbf q_*$ and $\mathbf p_*$, we check in ball arithmetic that the point lies off the exceptional hypersurface of \S\ref{ss:d5} and that $m_o\ne m_a+m_b$ on every triangle $T=\{o,a,b\}$ with $\lab{E}(T)$ in the label set. We also show in ball arithmetic that no body of such a triangle is at its centre of mass, except at the triangles in the centred case, whose masses are exactly proportional to $(\frac14,1,1)$. Each factor of the hypersurface needed at these triangles is enclosed in a ball that excludes $0$.

This point check covers $88$ applications of $\VN$, including all those used in the proof. Each of them lies off the factors of the hypersurface needed at its triangles (in the centred case of \S\ref{ss:d5} only those of (R2) for the two other bodies of $T$, by the model of that case in the supplementary material) and satisfies the second condition. Thirteen of them have a triangle of masses $(\mu/4,\mu,\mu)$, in the centred case.

The enumerations of the cells of the prevarieties of \S\ref{ss:Ksystems} make $13609$ linear-programming decisions for $\mathrm{K14}$ and $32010$ for each system $\mathrm{K15}$. The final checks of the point records of Table~\ref{tab:points} concern $4$ distinct pairs $(S,T)$.

\subsection{Cross-checks}\label{ss:crosschecks}
\begin{itemize}
\item \emph{Pieces $\pc{d15}$, independently of Corollary~\ref{cor:nod15}.}
\begin{enumerate}[label=\textup{(\alph*)}]
\item At the points of Table~\ref{tab:points}, and at the other mass points of \S\ref{sec:curves} at which $\mathrm{K14}$ is used in the proof, the system $\mathrm{K15}(m_{Q_j},k)$ has no solution, by runs of Theorems~\ref{thm:KA} and~\ref{thm:KApar}(b), for each piece $\pc{d15}(j,k)$ removed by the certificate of the point. At the points of Table~\ref{tab:points} these runs and those of $\mathrm{K14}$ exclude all pieces $\pc{d14a}$, $\pc{d14b}$ and $\pc{d15}$ of the clusters of the transversals from the cluster systems alone, independently of \S\ref{sec:energy}.
\item The system $\mathrm{K15}((1,1,1,\nu),k)$ in the normalization of \S\ref{ss:Ksystems}, with $\nu$ as an unknown, has exactly $768$ solutions when $k$ is the body of mass $\nu$ and exactly $1448$ when $k$ has mass $1$. They lie over the roots of irreducible polynomials of degrees $128$ and $724$, each with exactly two positive roots. The proof counts the solutions modulo a prime and excludes the open cells of the prevariety by a local analysis, at two primes.
\item At the four resulting values of $\mu$ on the line $\mathrm{RL}$, and at the two values of $t$ on $T_2$ at which $t^2$ is a positive root of the second polynomial, a nonzero coefficient of order at most $3$ in a weighted form of the rows excludes a place of type $\pc b_k(j)$ at each leading point, $288$ leading points when $k$ is the body of mass $\nu$ and $96$ otherwise, at three primes. With the previous item, this excludes the pieces $\pc{d15}(2,k)$ on $\mathrm{RL}$ and $\pc{d15}(1,k)$, $k=3,4,5$, on $T_2$.
\item No solution of $\mathrm{K15}((1,1,t,t),k)$, $t\in\C^*$, has a bad shape. For $k=1$, all solutions of this system with $t$ as an unknown, in a normalization, have unit coordinates at the prime $2147483629$, by its prevariety and a local analysis at two of its cells. Two standard bases modulo that prime, of the system with the condition of a bad shape added, are the unit ideal. The other values of $k$ reduce to $k=1$. This excludes the pieces $\pc{d15}$ of the transversal cluster on $T_1$ and on $T_7$.
\item Along $T_9$, let $Z_k$ be the set of $s$ at which $\mathrm{K15}(m_{Q_1},k)$ has a torus zero. Then $Z_2=Z_1$, by the exchange of the two bodies of mass $\rho_0$, and $Z_4\cap Z_1=Z_4\cap Z_3=\emptyset$, by the cells of the three systems modulo $2147483629$ and by polynomials $u_4$, $u_1$, $u_3$ in $s$ in their ideals with $\gcd(u_4,u_1)=\gcd(u_4,u_3)=1$. Hence at every point of $T_9$ one of the two certificates for the generic label set applies without Corollary~\ref{cor:nod15}.
\end{enumerate}
\item \emph{Proposition~\ref{prop:eqfull}.} A standard basis over $\Q(\jj)$ of the system of Proposition~\ref{prop:eqfull}, with $\nu$ as an unknown and saturated by $\prod p_{il}\cdot\nu(3+\nu)$, is $\{1\}$. This confirms the proposition whenever $\nu(3+\nu)\ne0$. An independent encoding of the system gives the same result. With $c=d=0$ it finds the expected solutions of $\mathrm{K14}$.
\item \emph{Theorem~\ref{thm:D14} as used in Proposition~\ref{prop:T458}.} On the families $T_4$, $T_5$ and $T_8$ we confirm the exclusion of the pieces $\pc{d14b}(1,k)$ of the transversal cluster $Q_1$, for $k=2,\dots,5$ on $T_4$ and $k=4,5$ on $T_5$ and $T_8$, with Lemma~\ref{lem:d14blead}, the description of the configurations that leads to \eqref{eq:tsys}, and Lemma~\ref{lem:typeIII}, but without the rest of the proof of Theorem~\ref{thm:D14}. These are the pieces $\pc{d14b}$ of the minimal exclusion sets of \S\ref{ss:T458} that use only $Q_1$. By Lemma~\ref{lem:d14blead}, at a place with type in the attained set of $\pc{d14b}(1,k)$ the leading coefficients of the cluster form a $\mathrm{K14}(m_{Q_1})$ configuration that satisfies $\mathrm{X3}_k$ (\S\ref{ss:d14}), after the exchange of the colours if necessary: body $k$ lies at the $z$- or the $w$-centre of mass of $Q_1$. We show that at no point of these families does a $\mathrm{K14}(m_{Q_1})$ configuration satisfy $\mathrm{X3}_k$ in $z$ or in $w$. With $d_{il}=z_{il}w_{il}$ and $M_Q$ the mass of the cluster, the parallel-axis identity shows that $\mathrm{X3}_k$, in $z$ or in $w$, is equivalent to $M_Q\sum_lm_ld_{kl}=\sum_{i<l}m_im_ld_{il}$. By Lemma~\ref{lem:typeIII}, a non-collinear configuration at positive masses has a pattern of type I or II. By complex conjugation four of these seven classes suffice. At positive masses $\kappa\ne0$ in \eqref{eq:tsys} and the masses are then rational functions of $t$. A collinear configuration solves one of $32$ tournament systems $\sum_{l\ne i}m_ls_{il}/z_{il}^2=0$, $s_{il}=\pm1$, linear in the masses. In suitable labels $T_4$ and $T_5$ lie in the plane $m_3=m_4$ of the cluster masses. An explicit resultant $P_T$, of degree $6$ for $T_4$ and $12$ for $T_5$, vanishes on each family. For each of the four classes, every needed $k$ and each tournament we compute with Singular~4.4.1, in characteristic $0$, a standard basis over $\Q(\jj)$ of the ideal $J$ of the configurations with $\mathrm{X3}_k$ in this plane, and show that $P_T$ is a unit modulo $J$. We establish each unit statement by an exact standard basis of $J+P_T$ in characteristic $0$. Those for the four classes we establish also modulo the prime $p'=536870879$, by the following modular test: if a Gr\"obner basis of $J$ has $p'$-integral coefficients \textup{(H2)} and leading coefficients that are nonzero modulo $p'$ \textup{(H3)}, then its reduction is a Gr\"obner basis of the reduced ideal with the same staircase, the multiplication matrices reduce accordingly, and a unit modulo $p'$ is a unit. On $T_8$, where no two masses are identically equal, every point is a zero of an explicit polynomial $P_{T_8}$ in the masses of the bodies $3$ and $5$ and the parameter $r$. We write the systems in the same way, with the mass relations of $T_8$ in place of the plane. The ideal $J$ is then not saturated, so that $V(J)$ may contain points that are not configurations. For the collinear configurations and for three of the four classes, $P_{T_8}$ is a unit modulo $J$, by a standard basis in characteristic $0$ followed by the modular test at $p'$ and, except for two of the classes with $\mathrm{X3}_4$, at the prime $p=536870909$. For the fourth class $P_{T_8}$ is not a unit modulo either prime, but it vanishes on $V(J)$ only where a coordinate $t_i$ vanishes. At each configuration $t_i\ne0$. For this class we use the following extension of the modular test, with $f=t_i$. Let $A=\Q(\jj)[x]/J$, and let $\bar a$ be the dimension of the generalized eigenspace of multiplication by $\bar f$ for the eigenvalue $0$ on the reduction of $A$. If \textup{(F1)} $\dim A/f^NA=\bar a$ for some $N$ and \textup{(F2)} $\bar f$ is nilpotent modulo $\bar J+(\bar P_{T_8})$, then $P_{T_8}$ has no zero on $V(J)\setminus V(f)$. Indeed, the characteristic polynomial of multiplication by $f$ is $\lambda^a\chi_1$ with integral coefficients and $\chi_1(0)\ne0$. Condition \textup{(F1)} gives $a=\bar a$, so that $\chi_1(0)$ is a unit at the prime. So the idempotent of $A$ on which $f$ is invertible is integral and reduces to the corresponding idempotent of the reduction, on which $\bar P_{T_8}$ is invertible by \textup{(F2)}. Hence $P_{T_8}$ is invertible on the part of $A$ where $f$ is invertible. Here \textup{(F1)} holds with $\bar a=6$ and $N=3$, for $\mathrm{X3}_4$ and for $\mathrm{X3}_5$. Conditions \textup{(F2)}, \textup{(H2)} and \textup{(H3)} are checked at both primes. Each unit statement that we establish modulo a prime has a modular test in which we check \textup{(H2)} and \textup{(H3)} element by element. We derive the systems twice, independently. The two derivations agree.
\item \emph{Lemma~\ref{lem:typeIII}.} We check the identity for $h_{abc}$ in the proof of Lemma~\ref{lem:typeIII} by machine for each of the four sets $\{a,b,c\}$ of three bodies. A second proof of the lemma, by an explicit parametrization of the solutions of \eqref{eq:tsys} of type III, is in the supplementary material. We also ran the computations of the previous item for the classes of type III on $T_4$ and $T_5$, and on $T_8$ for $\mathrm{X3}_5$. They agree with the lemma. On $T_4$ and $T_5$, $P_T$ is a unit modulo $J$. On $T_8$, for $\mathrm{X3}_5$, the case $D=0$ for a polynomial $D$ of the class gives a unit. In the case $D\ne0$, where one unknown is eliminated through $D\ne0$, the extension of the modular test applies with $f=D$, $\bar a=192$ and $N=4$.
\item \emph{Theorem~\ref{thm:D14} as used in Theorems~\ref{thm:T1T7}, \ref{thm:T2}, \ref{thm:RL} and Proposition~\ref{prop:farT9}.} With Lemma~\ref{lem:d14blead} and the condition $\mathrm{X3}_k$, in $z$ or in $w$, but without the rest of the proof of Theorem~\ref{thm:D14}, we exclude the pieces $\pc{d14b}$ of the transversal cluster used in Theorems~\ref{thm:T1T7}, \ref{thm:T2} and~\ref{thm:RL} and Proposition~\ref{prop:farT9}. On $T_1$ and $T_7$, off the sixteen special values of $c$, $\mathrm{K14}(m_{Q_1})$ has no solution. At every configuration of Lemma~\ref{lem:K14FAFB} for $F_B$ we evaluate $\mathrm{X3}_k$ in $z$ and in $w$ in ball arithmetic for the four positions $k$; no ball contains $0$. If a $\mathrm{K14}(1,1,1,\nu)$ configuration with $\nu\ne0$ satisfies $\mathrm{X3}_k$, then $k$ is the body of mass $\nu$ and $3\nu^2=\pm1$. Indeed, in a normalization of the gauge either $z=w$ or the matrix $A$ of the derivation of \eqref{eq:tsys} has rank one. In each case $\mathrm{X3}_k$ adds one equation. We compute the eliminations with Singular~4.4.1, over $\Q(\jj)$ for the $2\times9\times2$ systems of the second case and over $\Q$ for the $2\times32$ of the first, and recompute all of them with Macaulay2~1.25.11. Only $k=4$ with $3\nu^2=1$ (one system) and $3\nu^2=-1$ (four systems) survive. This excludes $\pc{d14b}(1,k)$, $k=3,4,5$, on $T_2$, and all $\pc{d14b}(2,k)$ on $\mathrm{RL}$ except $\pc{d14b}(2,5)$ at $\mu=\mu^*=4/\sqrt3$. There $\mathrm{K14}$ at $(4,4,4,\mu^*)$ has exactly two configurations up to the gauge, the equilateral triangle of the bodies $1$, $3$, $4$ with body $5$ at its centre and its mirror image. The places on the segment of $\pc{d14b}(2,5)$ have exactly $96$ leading points, $48$ over each configuration. The exchange of the bodies $3$ and $4$ maps one half to the other. A weighted form of the rows that does not depend on the parameter $\sigma\in(1,2)$ of the segment, followed by a Lyapunov--Schmidt reduction, gives at each of the $48$ leading points over one configuration a series $g(\delta)$ that must vanish. Modulo two primes, with all inverses checked to be units, $g$ has a nonzero coefficient of order at most $5$. Along $T_9$, $\mathrm{K14}(m_{Q_1})$ together with the condition of Lemma~\ref{lem:d14blead} for body $k$ has no torus zero for any $s\in\C^*$, by Theorem~\ref{thm:KApar}(a) (four systems, two primes).
\item \emph{The inclusions in the proof of Theorem~\ref{thm:types}, all labellings.} For all $120$ labellings, each type set of Table~\ref{tab:types} lies in the attained set of its piece in Table~\ref{tab:pieces}, with diagram~$7$ refined by Table~\ref{tab:d7}. Three programs check this in exact rational arithmetic: for diagrams $1$, $4$, $7$, $8$ and $10$--$13$, for the refined diagram~$7$, and for diagrams $2$, $3$, $6$, $9$ and $14$--$16$.
\item \emph{Theorem~\ref{thm:hulls}.} Exact computations confirm Theorem~\ref{thm:hulls}. For each assertion of Propositions~\ref{prop:d5empty}--\ref{prop:d5VN}, and for each main step of their proofs, a list of relations of the model that contains those used in it, together with its negated conclusion, forms a system of linear relations and disjunctions. Two programs show that each of these systems is infeasible, by exact certificates. One program takes the relations from the programs that define the models; the other builds the models anew and uses its own exact linear programming. Independently, for every pair of modes of $\Vtwo^{\mathrm w}$, $\Vtwo$ and $\VN$, a complete branching over the disjunctions of the model, with an exact certificate at every node, shows that the projection of the model lies in the polytope of Table~\ref{tab:d5hulls}, or that the model is empty. The same holds for the model of the centred case on its four pairs of modes. A separate checker extracts each model again and verifies all these certificates. Moreover, every vertex $v$ of each polytope of Table~\ref{tab:d5hulls} is a limit of projections of model points: exact points $x_s$ of the model and $x_c$ of its closure, with $x_c$ projecting to $v$, have the half-open segment $(x_c,x_s]$ in the model. So each polytope is the convex hull of the closure of the projection of its model.
\end{itemize}

\subsection{Formalization}\label{ss:formal}
Theorem~\ref{thm:main} is proved in Lean~4 with Mathlib (project \texttt{lean\_full}, commit \texttt{52858e1}; toolchain v4.35.0-rc3, Mathlib commit \texttt{c55e6e7}). The formal statement asserts that for every $m\in(\R_{>0})^5$ there is a finite set of configurations in $\C^5$ such that every solution of \eqref{eq:cc} by distinct points, with $\lambda\in\R$ and $c\in\C$, is the image of one of them under a map $z\mapsto az+b$ or $z\mapsto a\bar z+b$ with $a\ne0$. Admitting reflections does not change finiteness. The proof uses only the axioms propext, Classical.choice and Quot.sound, and no evaluation by compiled code. It is also accepted by nanoda and lean4lean, two independent implementations of the Lean kernel.

The formal proof does not assume the statements of \S\ref{ss:akinputs}. It proves at singular places what it needs of them, among them the rules of \cite{AK12} and the classification of \cite[\S7]{AK12}: a search in the kernel finds $1376$ labelled diagrams that satisfy the rules, which are, up to relabelling and the exchange of the colours, the sixteen diagrams of \cite[Fig.~11]{AK12} and eight others; it excludes the eight at places. Data produced by our programs enter only as certificates checked in the kernel, among them the lexicographic certificates, the flats of Theorem~\ref{thm:S}, the runs and enumerations of $\mathrm{K14}$, the resultants of Theorem~\ref{thm:gate} and the branch and bound of \S\ref{sec:rays}, which $83454$ generated modules replay, with local repairs where a test fails in the arithmetic of the kernel. The formal proof of Theorem~\ref{thm:D14} does not use Proposition~\ref{prop:P11}, and it replaces Propositions~\ref{prop:D14N} and~\ref{prop:resonant} by arguments of the same kind for $\sigma<5/3$ and for $\sigma>11/7$: these ranges cover $(1,2)$, so the resonant values of $\sigma$ play no role. In the formal proof, relation (R2) of \S\ref{ss:d5} follows from one polynomial identity and $36$ factorizations instead of eliminations. Building the project from a fresh copy of its repository takes about $860$ CPU-hours; the supplementary material gives the commands.

\subsection{Hand proofs and computations}
The arguments we give by hand do not depend on any machine check; programs re-verify steps of many of these arguments (see the supplementary material).

\smallskip\noindent\emph{Arguments that need no computer}, among others:
\begin{itemize}
\item the proofs of Lemma~\ref{lem:infty}, Propositions~\ref{prop:G1} and~\ref{prop:G2} and Theorems~\ref{thm:wtriangle}, \ref{thm:D9} and~\ref{thm:hulls};
\item the exclusion of diagram~$15$ (Corollary~\ref{cor:nod15}) apart from the identities marked $(\dagger)$ in the proof of Proposition~\ref{prop:eqfull};
\item steps in the proof of Lemma~\ref{lem:classI};
\item the levels of the expansion in Lemmas~\ref{lem:d14exp} and~\ref{lem:d14energy};
\item the identities in the proofs of Propositions~\ref{prop:D14N} and~\ref{prop:resonant}.
\end{itemize}

\smallskip\noindent\emph{Computations without a hand proof}: the computations used in the proof, among them
\begin{itemize}
\item the computations of Theorem~\ref{thm:S} (Proposition~\ref{prop:Stree}) and of Proposition~\ref{prop:Spoints};
\item the computational steps of the proof of Theorem~\ref{thm:gate} (Appendix~\ref{app:d2});
\item the point certificates of \S\ref{sec:points};
\item the certificates of \S\ref{sec:curves};
\item the computational steps of the proof of Theorem~\ref{thm:D14}.
\end{itemize}
The formal proof of \S\ref{ss:formal} depends neither on the statements of \S\ref{ss:akinputs} nor on the correctness of the mathematics software named above. It depends on the Lean kernel and on the formal statement, which the reader can compare with Theorem~\ref{thm:main} in the file \texttt{CC5Full/System.lean} of the project (with \texttt{Masses} from \texttt{CC5Full/Basic.lean}); the proof is the theorem \texttt{CC5Full.Core.Compose.MainTheorem\_holds}.