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

The proofs of the statements marked $\dagger$ include computations. All other proofs are by hand. Tables~\ref{tab:verif}--\ref{tab:verif4} list the computations, the software on which they depend and the checks made of them. The software is Singular \cite{DGPS}, msolve \cite{BES21}, gfan \cite{Jen}, FLINT \cite{FLINT} and its ball arithmetic Arb \cite{Joh17} through python-flint, Macaulay2 \cite{GS}, HiGHS \cite{HH18}, SymPy \cite{SymPy} and mpmath, and for \S\ref{ss:lean} Lean~4 with Mathlib. The programs, certificates and logs are in the supplementary material, available at \url{https://doi.org/10.5281/zenodo.23472605}, which also gives the versions of the software. It holds the programs of Sections~\ref{sec:diagrams}--\ref{sec:exclusion} at one pinned version, with the list of changes made after the runs, none of which affects their results.

\begin{table}[tp]
\centering
\footnotesize
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{2.2cm}>{\raggedright\arraybackslash}p{6.4cm}>{\raggedright\arraybackslash}p{6.5cm}@{}}
\toprule
statement & computation and trusted software & checks\\
\midrule
Prop.~\ref{prop:enum} & exhaustive search (Python) & $41$ diagrams in $5$ classes for $n=4$; $1376$ in $24$ classes for $n=5$, as in the kernel-checked search of \cite[\S12.4]{Tom26}; contains the $117$ of \cite{CC23}. An enumeration that assembles the diagrams from their connected components, written from the statements of the rules independently of the program, finds the same diagrams for $n=4,5,6$, class by class\\
Prop.~\ref{prop:cells} & depth-first search in $384$ parts per class; linear programs solved in floating point (HiGHS); each of the $76{,}087{,}734$ prunes certified by Lemma~\ref{lem:farkas} in rational arithmetic, from a dual solution, a dual ray or an exact simplex method in python-flint. The count includes the repetitions of the first two insertions in every part & a rerun of the same programs on seven classes ($33{,}502$ cells) reproduces the cells exactly. Deliberately invalid certificates are rejected. The smallest slack is $0.0055$ over all programs judged feasible and $0.0345$ over the listed cells. The largest optimal slack of a pruned program is $1.4\cdot10^{-14}$\\
Prop.~\ref{prop:exclusion}, argmin sets & $184{,}997{,}938$ decisions on argmin sets, each certified by Lemma~\ref{lem:farkas} & the generators of the identities and initial forms used by the programs, evaluated at three complex solutions for six bodies, sum to less than $6\cdot10^{-14}$, and the exponents of $784{,}228$ terms agree with the sums of the exponents of their factors; in Lean (\S\ref{ss:lean}): each single term and each argmin set used by a core certified again\\
Prop.~\ref{prop:exclusion}, cores & cores searched modulo $32003$ (not trusted) and certified by standard bases over $\Q(m)$, in the second pass with one mass set to $1$, without saturation (Singular) & Macaulay2 confirms $2{,}403$ of the $2{,}413$ cores: $2{,}394$ with all six masses as parameters and $5$ with one mass set to $1$, both with the saturation by $\Theta$ through an extra variable $t$ and the polynomial $t\Theta-1$, $3$ by checking in polynomial arithmetic cofactors, computed in Singular with one mass set to $1$, that express $1$ in the ideal generated by the core and $t\Theta-1$, and $1$ by showing, with one mass set to $1$, that the core itself generates the unit ideal. It corroborates the other ten at two random rational mass points each. For $40$ random cores of the first pass, cofactors of the same kind with all six masses as parameters, at most $1.7$~MB, pass the same check. For five bodies, the initial system of the cell of diagram~$5$ of \cite[Fig.~11]{AK12} that contains a place of the continuum of \cite{Rob99} does not generate the unit ideal at the masses $(\frac12,\frac12,\frac12,\frac12,-\frac18)$, proportional to the masses $(1,1,1,1,-\frac14)$ of the continuum, modulo $32003$ and over $\Q$, and generates it at random masses\\
Prop.~\ref{prop:exclusion}, identities & identities $\sum_ic_if_i=h$ with integer polynomials for $1{,}928$ distinct cores ($1{,}900$ of the $1{,}935$ distinct stored cores and $28$ other subsets of initial systems, \S\ref{ss:lean}), computed by Singular (\texttt{lift}, \texttt{liftstd} or elimination) and checked in Lean & in Lean (\S\ref{ss:lean}): each identity checked by expansion, with the initial forms recomputed from the trees\\
\bottomrule
\end{tabular}
\caption{Computations of Sections~\ref{sec:diagrams}--\ref{sec:exclusion} and their checks.}\label{tab:verif}
\end{table}

\begin{table}[tp]
\centering
\footnotesize
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{2.6cm}>{\raggedright\arraybackslash}p{6.2cm}>{\raggedright\arraybackslash}p{6.3cm}@{}}
\toprule
statement & computation and trusted software & checks\\
\midrule
Lemma~\ref{lem:three} & hand proof & eliminations in Singular at $(1,2,7)$, $(1,2,8)$ and $(2,3,11)$, compared with $S_\mu$ in SymPy, and in a second formulation at $(1,2,7)$, $(2,9,4)$ and $(3,5,13)$\\
Lemma~\ref{lem:dominant} & hand proof & at $(1,2,40)$: the bounds of the first statement in exact arithmetic, and the roots and $\rho$ numerically (SymPy, mpmath); at $(1,2,7)$: root enclosures and bounds in Arb (python-flint) and in exact rational arithmetic with Rouch\'e disks; a third program in mpmath; a direct test of all signed sums, in the Arb program\\
Thm.~\ref{thm:d93} & factorization in $\Q[\mu]$ (Singular) & the terms printed in \cite[p.~574]{AK12}, and a nonzero value at $(1,2,7)$ (SymPy)\\
Lemma~\ref{lem:d88comp}(a) & initial forms and coefficients (SymPy); prevarieties (gfan~0.7); cone tests (Singular) & a separate program computes the prevarieties with exact certificates and finds the same $2149$ and $224$ face vectors, with all cone tests redone in msolve. As a check that the tests can find nonempty cones, both find six for $S_{12}$ at the masses $(1,1,2,2)$, and the separate program finds one for $\mathrm{KC}$ at $(1,1,1,5)$\\
Lemma~\ref{lem:d88comp}(b) & systems written by SymPy; Gr\"obner bases modulo $p$ (msolve) & in Lean (\S\ref{ss:lean}): the upper bounds, checked by the kernel from traces of runs of an F4 algorithm written in Lean, with bases that have the same leading monomials as those of msolve. Outside Lean: the same leading ideal modulo $2^{31}-1$ from msolve, $20{,}316$ and $4788$ from Macaulay2 (F4), and $4788$ from Singular\\
Lemma~\ref{lem:d88comp}(c), (d) & Krawczyk test in Arb & interval arithmetic in mpmath with forward differentiation (for (d) the square roots are bounded with a safety factor instead of outward rounding); a third, rigorous implementation from separately derived equations. Both check that the boxes are pairwise disjoint\\
\S\ref{ss:d88}, last paragraph & the test of Lemma~\ref{lem:Ttest}(a) over the bodies $1,2,3$ on the boxes of Lemma~\ref{lem:d88comp}(d), in interval arithmetic (mpmath); $|Y_4|$ and $\max_{l\le3}|Y_l/Y_4|$ at the $36$ solutions with relative margin below $10^{-4}$, at the centres of the boxes & the same count in floating point at the centres of the boxes\\
\bottomrule
\end{tabular}
\caption{Computations of Section~\ref{sec:ak50} and their checks.}\label{tab:verif2}
\end{table}

\begin{table}[tp]
\centering
\footnotesize
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{2.6cm}>{\raggedright\arraybackslash}p{6.2cm}>{\raggedright\arraybackslash}p{6.3cm}@{}}
\toprule
statement & computation and trusted software & checks\\
\midrule
Lemma~\ref{lem:E4cert} & hand proof; the resultants $R_1$, $R_2$, $\Res_t(R_1,R_2')$ of the proof (SymPy) & at $(1,1,1,1)$: standard bases over $\Q(\mathrm j)$ and $\Q$ (Singular), ranks modulo $p$ (python-flint)\\
$E_4$ at $(3,5,7,11)$ (\S\ref{ss:E4}) & ranks modulo $p$ (python-flint) & standard bases over $\Q(\mathrm{j})$ and $\Q$ (Singular); Macaulay2\\
Lemma~\ref{lem:C4cert} & unit ideals modulo $32003$ (Singular) & msolve modulo $1073741789$; Macaulay2 modulo $1000003$\\
$C_4$ at $(1,1,1,1)$ (\S\ref{ss:k4diagrams}) & unit ideals modulo $32003$ (Singular) & msolve modulo $1073741789$\\
Rem.~\ref{rem:BEsums} & standard bases over $\Q$, with saturation (Singular) & ranks of Macaulay matrices modulo $p$ (python-flint) are deficient for the same numbers of patterns\\
\bottomrule
\end{tabular}
\caption{Computations of Section~\ref{sec:k4} and their checks.}\label{tab:verif3}
\end{table}

\begin{table}[tp]
\centering
\footnotesize
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{2.6cm}>{\raggedright\arraybackslash}p{6.2cm}>{\raggedright\arraybackslash}p{6.3cm}@{}}
\toprule
statement & computation and trusted software & checks\\
\midrule
Prop.~\ref{prop:cliquecount} & count of the cliques of Corollary~\ref{cor:cliquecell} in the stored cells (Python) & rerun from the stored cells; checked in Lean (\S\ref{ss:lean})\\
Prop.~\ref{prop:handcover} & checks of the hypotheses of the lemmas of Section~\ref{sec:hand} on the stored cells (Python); argmin sets of further identities certified by Lemma~\ref{lem:farkas}; the polynomials of Lemmas~\ref{lem:handW3} and~\ref{lem:handEQ2} in the $74$ cells where they are used (SymPy); the minors of Lemma~\ref{lem:handLIN} at three mass points & a second program, written from the statements of the lemmas independently of the first, puts every cell in the same group as the first for the lemmas other than Corollary~\ref{cor:cliquecell} and recertifies the argmin sets of the further identities in rational arithmetic. On the polyhedra of the second program, a linear program in floating point confirms the conclusions of Lemmas~\ref{lem:handT}--\ref{lem:handC} in every cell where they apply. Eliminations with saturation in Singular give the polynomials of the triangle lemmas\\
\bottomrule
\end{tabular}
\caption{Computations of Section~\ref{sec:hand} and their checks.}\label{tab:verif4}
\end{table}

\begin{table}[tp]
\centering
\footnotesize
\begin{tabular}{@{}lr@{}}
\toprule
result & cells\\
\midrule
Corollary~\ref{cor:cliquecell} & $86{,}938$\\
Corollary~\ref{cor:handE1} & $86{,}875$\\
Lemma~\ref{lem:handR}(a), (b) & $79{,}318$\\
Lemma~\ref{lem:handR6} & $54{,}208$\\
Lemma~\ref{lem:handC} & $46{,}289$\\
Lemma~\ref{lem:handT} & $40{,}084$\\
Corollaries~\ref{cor:cliquecell} and~\ref{cor:handE1}, both & $84{,}155$\\
at least one of Corollaries~\ref{cor:cliquecell} and~\ref{cor:handE1} & $89{,}658$\\
\midrule
cells excluded at every positive mass, at least & $71{,}235$\\
\quad by Proposition~\ref{prop:handcover}(a), a lower bound & $70{,}406$\\
\quad by Lemma~\ref{lem:single}, other cells & $771$\\
\quad by Theorem~\ref{thm:d89}, diagram~$89$ & $49$\\
\quad by Proposition~\ref{prop:d82}, further cells of diagram~$82$ & $9$\\
\bottomrule
\end{tabular}
\caption{The results of Section~\ref{sec:hand} that apply most often, with the numbers of cells of Proposition~\ref{prop:handcover} to which they apply, and the cells that Sections~\ref{sec:exclusion}, \ref{sec:ak50} and~\ref{sec:hand} exclude at every positive mass.}\label{tab:handuse}
\end{table}

Three remarks qualify the tables. First, as noted in Section~\ref{sec:exclusion}, the cores of Proposition~\ref{prop:exclusion} were computed and certified without saturation: the saturations that the programs request, by $E$ and the leading coefficients of the positions in the search and by the factors of $\Theta$ in the variables of the core in the certification, were not carried out. There are $2{,}413$ certified cores: $1{,}423$ from the first pass, counted as distinct within each class, and $990$ from the second. The cells with a core are checked in Lean through Lemma~\ref{lem:core}(a) ($37{,}824$ cells) or Lemma~\ref{lem:core}(b) ($974$ cells). Macaulay2 confirms all but ten of the cores, which are among those of the second pass and belong to eight cells of diagram~$7$ and to one cell each of diagrams $14$ and $16$. The identities checked in Lean (\S\ref{ss:lean}) remove the Gr\"obner basis computations from the trusted base of the exclusion of the $38{,}798$ cells with a core. They include the ten cells above, six of them through another subset of the same initial system.

Second, msolve prints the leading monomials of the Gr\"obner bases of Lemma~\ref{lem:d88comp}(b), not the bases, so the upper bounds for the dimensions cannot be checked from its output. They are checked by Lean's kernel, from traces of the runs of an F4 algorithm written in Lean (\S\ref{ss:lean}). The matching lower bounds need no Gr\"obner basis: the boxes of (c) and (d) give $20{,}316$ and $4788$ distinct zeros at $\mu_0$, respectively, and the fibre dimension of the finite module in Lemma~\ref{lem:goodred} is upper semicontinuous.

Third, the programs that generate the identities, the exponents of their terms and the initial forms, and those that check the certificates of Lemma~\ref{lem:farkas}, are tested as in Table~\ref{tab:verif}. The former compute the exponents in binary floating point, which is exact here because all their coefficients are small dyadic rationals, and the latter use exact rational arithmetic. Apart from these exponents and from decisions of feasibility, the computations of the proof use floating point only to propose certificates or approximate zeros, which are then checked in exact or ball arithmetic. Feasibility is not certified in the runs of the linear programs, but an error there could only add a cell to the list or remove an identity from an initial system.

\subsection{The formal proof in Lean}\label{ss:lean}
We have formalized Theorem~\ref{thm:main} in Lean~4 with Mathlib. The formal proof is the theorem \lean{CC6Compose.V4.main_theorem_v4}, whose statement is \lean{CC6Full.MainTheorem}. This Lean theorem has no hypotheses. The definitions are those of the file \lean{CC6Full/Statement.lean}, shown here without comments and with one line break changed (namespace \texttt{CC6Full}, with \texttt{open Finset}):
\begin{alltt}\footnotesize
abbrev Conf (n : \(\mathbb{N}\)) := Fin n \(\to\) \(\mathbb{C}\)
def CollisionFree \char123{}n : \(\mathbb{N}\)\char125{} (q : Conf n) : Prop := \(\forall\) i j, i \(\ne\) j \(\to\) q i \(\ne\) q j
def IsCC \char123{}n : \(\mathbb{N}\)\char125{} (m : Fin n \(\to\) \(\mathbb{R}\)) (q : Conf n) : Prop :=
  CollisionFree q \(\wedge\) \(\exists\) (lam : \(\mathbb{R}\)) (c : \(\mathbb{C}\)), \(\forall\) i,
    ((lam * m i : \(\mathbb{R}\)) : \(\mathbb{C}\)) * (q i - c) =
      \(\sum\) j \(\in\) univ.erase i, ((m i * m j / \(\|\)q i - q j\(\|\) ^ 3 : \(\mathbb{R}\)) : \(\mathbb{C}\)) * (q i - q j)
def Similar \char123{}n : \(\mathbb{N}\)\char125{} (q q' : Conf n) : Prop :=
  \(\exists\) a b : \(\mathbb{C}\), a \(\ne\) 0 \(\wedge\)
    ((\(\forall\) i, q' i = a * q i + b) \(\vee\) (\(\forall\) i, q' i = a * starRingEnd \(\mathbb{C}\) (q i) + b))
def FinitelyManyCC \char123{}n : \(\mathbb{N}\)\char125{} (m : Fin n \(\to\) \(\mathbb{R}\)) : Prop :=
  \(\exists\) F : Finset (Conf n), \(\forall\) q, IsCC m q \(\to\) \(\exists\) q' \(\in\) F, Similar q' q
def GenericFiniteness (n : \(\mathbb{N}\)) : Prop :=
  \(\exists\) F : MvPolynomial (Fin n) \(\mathbb{Z}\), F \(\ne\) 0 \(\wedge\)
    \(\forall\) m : Fin n \(\to\) \(\mathbb{R}\), (\(\forall\) i, 0 < m i) \(\to\) MvPolynomial.aeval m F \(\ne\) 0 \(\to\) FinitelyManyCC m
def MainTheorem : Prop := GenericFiniteness 6
\end{alltt}
The plane is $\C$, and body $k$ of the paper is \texttt{k - 1 : Fin n}. \texttt{IsCC m q} is \eqref{eq:cc} for a configuration of distinct points, with $\lambda\in\R$ and $c\in\C$: the sum over \texttt{univ.erase i} runs over $j\ne i$, and $\|q_i-q_j\|$ is the distance. Since \texttt{starRingEnd}~$\C$ is complex conjugation, \texttt{Similar} admits reflections. This does not change finiteness, because the complex conjugate of a central configuration is again one. \texttt{MvPolynomial.aeval m F} is the value $F(m)$, so \texttt{MainTheorem} is Theorem~\ref{thm:main}. The theorem \lean{exists_pos_aeval_ne_zero} shows that a nonzero $F\in\Z[m_1,\dots,m_n]$ does not vanish at some positive mass vector, so the statement is not vacuous. The formal statement does not describe $F$. In particular, what Section~\ref{sec:intro} and Remarks~\ref{rem:P98set} and~\ref{rem:BEsums} say about the zero set of $F$, the polynomial of Section~\ref{sec:proof}, is not formalized.

The formal proof has three parts. The first is the framework \texttt{CC6Full}, which formalizes the theory of Sections~\ref{sec:setup}--\ref{sec:proof}. For any number of bodies it constructs, from infinitely many central configurations, a \emph{germ} with $\ell\le0$, following \S\S\ref{ss:system} and~\ref{ss:places}. A germ is a solution of the equations of the bodies and the distance equations in Hahn series, with $U=E\ne0$ and with exponents normalized as in Lemma~\ref{lem:place}, and here it is given by the rotated expansions at a singular place. For germs, again for any number of bodies, the framework proves the identities of \S\ref{ss:identities}, Lemma~\ref{lem:initial}, the relations (O1)--(O6), the rules of Lemma~\ref{lem:rules}, the existence part of Lemma~\ref{lem:tree}, Lemma~\ref{lem:constraints}(b) and~(c), and Lemmas~\ref{lem:single} and~\ref{lem:core}. For six bodies it proves the results of Sections~\ref{sec:ak50} and~\ref{sec:k4} that Section~\ref{sec:proof} uses, with the computations at single mass points as hypotheses, and the reduction of Section~\ref{sec:proof} to the classes of diagrams. The second part consists of the two certificate projects, which check the computations of Sections~\ref{sec:diagrams}--\ref{sec:exclusion} and of Sections~\ref{sec:ak50} and~\ref{sec:k4}, respectively. The third is the package \texttt{CC6Compose}. It proves the bridges from the statements checked in the certificate projects to the hypotheses of the framework, which are statements about germs and polynomial systems, and it composes the main theorem. The bridges cover Propositions~\ref{prop:enum}, \ref{prop:cells} and~\ref{prop:exclusion}, the check that the representatives of the seven classes with the $43$ remaining cells are diagrams of Table~\ref{tab:ten}, Lemmas~\ref{lem:dominant}, \ref{lem:d88comp} and~\ref{lem:C4cert}, and the computation at $(3,5,7,11)$ in \S\ref{ss:E4}. The README of the framework lists, for each of these results, the certificate check and the bridge. Fourteen modules of \texttt{CC6Compose} that the formal proof does not import contain other assemblies of the theorem through checks by compiled code; two of them use the tactic \texttt{native\_decide}.

The formal proof departs from the proofs in this paper at the following places.
\begin{itemize}
\item Theorems~\ref{thm:d98}, \ref{thm:d93} and~\ref{thm:d88} rest on a lemma of integral elimination instead of resultants, constructible sets and the implicit function theorem. If the unknowns of a polynomial system over $\Q[\mu]$ are integral over $\Q[\mu][1/g]$ modulo the system, and the system has no complex solution at a rational point $\mu_0$ with $g(\mu_0)\ne0$, then some $h\in\Q[\mu]$ with $h(\mu_0)\ne0$ vanishes wherever the system has a solution and $g\ne0$. For diagrams $98$ and $93$ the integrality comes from the roots of $S_\mu$ and the square roots $c_{jl}$, respectively $\sqrt{Y_l}$, so the polynomials $\Phi$ and $\Phi_3$ and the resultants are not used. For diagrams $88$ and $94$ it comes from Lemma~\ref{lem:goodred}, and the empty fibre at the mass point $(\mu_0;m_5,m_6)$, with $\mu_0=(1,2,3,30)$ and with $(m_5,m_6)=(1,1)$ for diagram~$88$ and $(1,2)$ for diagram~$94$, replaces the implicit function theorem, the continuity of the tests and the density of real points.
\item Propositions~\ref{prop:E4} and~\ref{prop:C4} rest on a Macaulay transfer instead of the closedness of projections along projective space. If at $\mu_0$ every monomial of some degree, or bidegree, lies in the ideal of the forms, then some maximal minor $h(\mu)$ of the Macaulay matrix is nonzero. Wherever $h\ne0$, every monomial of that degree then lies in the ideal, so the forms have no common projective zero. This gives the polynomials $h_E$ and $h_C$ of Section~\ref{sec:proof} without showing that $B_E$ and $B_C$ are closed. The minor $h$ is not computed.
\item In place of Lemma~\ref{lem:E4cert}, which the certificate project also checks, the formal proof uses the computation at $(3,5,7,11)$ reported after Proposition~\ref{prop:E4}: the forms $\mathcal F_\varepsilon$ and $\mathcal G_\sigma$ have no common nonzero zero there, and the Nullstellensatz gives the monomials for the Macaulay transfer.
\item Lemma~\ref{lem:goodred} is proved with valuation rings instead of discrete valuation rings, since Mathlib provides valuation subrings that dominate a local ring but not discrete valuation rings that dominate a Noetherian local domain. The value group is then an arbitrary ordered abelian group. The tropical certificates of Lemma~\ref{lem:d88comp}(a) enter in torus form: the initial forms have no common zero in the torus over any field of characteristic $p$. The certificate project proves this for every ordered value group.
\item The identities of \S\ref{ss:identities}, Lemma~\ref{lem:initial}, the relations (O1)--(O6) and the rules of Lemma~\ref{lem:rules} are proved for germs, not for the expansions at a place.
\item Lemma~\ref{lem:C4cert} is used over $\F_{32003}$ only. The lemma states the unit ideals on the $14$ charts over $\F_{32003}$ and over $\F_{1073741789}$, but Lemma~\ref{lem:transfer} needs one prime, and the computation over $\F_{1073741789}$ is an independent check that the formal proof does not use.
\item The checks by the kernel take their inputs as Lean literals rather than as data files: the $191$ representatives of the classes, the certificates of the cores, and the sets $G$ and the cofactors of Lemma~\ref{lem:d88comp}(a). Checks by compiled code outside the formal proof relate these literals to the data files. No statement or proof of the formal proof reads text.
\item Propositions~\ref{prop:cells} and~\ref{prop:exclusion} are proved as one statement, checked by the kernel (see the list below). The cells of Proposition~\ref{prop:cells} appear only inside that check.
\item The test of Lemma~\ref{lem:Ttest} uses $|X_l|^{-1/2}$. In Lean $\|0\|^{-1/2}=0$, so $X_l\ne0$ is a separate hypothesis, which the certificate project checks at the zeros of Lemma~\ref{lem:d88comp}(c) and~(d).
\end{itemize}

The formal proof depends only on the three standard axioms \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}, as \texttt{\#print axioms} shows. There is no other axiom and no \texttt{sorry}. In particular the formal proof does not use the tactic \texttt{native\_decide}, which would add an axiom. So Lean's kernel checks the whole proof. It checks the computations by evaluation (the tactic \texttt{decide +kernel}).

A script of the framework builds the framework and the composition from scratch on top of the kernel checks of the two certificate projects. It checks that \lean{CC6Compose.V4.main_theorem_v4} depends on exactly these three axioms and that $47$ main theorems of the framework, \lean{exists_pos_aeval_ne_zero} among them, depend on no others, and it scans the sources, with the exemptions listed in the README of the framework, for keywords that could add an assumption or bypass the kernel. The kernel checks it uses come from earlier builds, which were verified against the committed sources and hashes before the script ran; the README of the framework describes these builds and their cost.

Each certificate project has a file \texttt{LEAN\_CHECKS.md} that lists the Lean theorems by the statements of this paper that they check, together with what each theorem assumes and what it costs. A check has two parts: a program on integers, rationals, lists and polynomials, and a theorem proved in Lean that turns the output of the program into a statement over $\C$, $\Z/p$ or a ring of polynomials. In these checks floating-point code is untrusted: it supplies centres, pivots, cofactors and certificates, and every test is exact. For the kernel the programs are written as structural recursions on lists and numbers, the data are given as Lean values rather than strings, and the untrusted parts of a computation, such as the rows and inverses of the Macaulay checks and the cofactors of the unit ideals, are given as data. The formal proof uses the following checks.
\begin{itemize}
\item Proposition~\ref{prop:enum}: the search, split into parts that the kernel checks one by one, lists every labelled diagram that satisfies the rules, and the $82{,}712$ diagrams are the disjoint union of the orbits of the $191$ representatives, which the check takes as a literal list.
\item Lemma~\ref{lem:farkas}, proved over every ordered field.
\item Propositions~\ref{prop:cells} and~\ref{prop:exclusion} together: for each class, and each pair of trees with heights that satisfies the conditions of Lemma~\ref{lem:constraints} for the representative and $\ell(x)\le0$, either the class is one of the seven classes that contain the $43$ remaining cells, or some identity has a single term of least exponent, as in Lemma~\ref{lem:single}, or the initial forms $f_i$ at the pair, written from the trees, satisfy one of $1{,}928$ identities $\sum_ic_if_i=h$ with integer polynomials, as in Lemma~\ref{lem:core}, where $h$ is a polynomial in the masses that is not zero at an explicit point. The kernel runs a form of the search of Proposition~\ref{prop:cells} written as total functions and proved in Lean to find every such cell, decides its linear programs by certificates accepted by Lemma~\ref{lem:farkas}, checks the claims in the cells it finds, and checks the identities by expansion. For $35$ cells the identity is for another subset of the initial system of the same cell, since Singular did not lift the stored core within the limits of time and memory tried. The framework and the bridges prove these conditions for germs, so this applies to the trees of a germ with $\ell\le0$.
\item The representatives of the seven classes that contain the $43$ remaining cells are diagrams of Table~\ref{tab:ten}, by evaluation in the kernel on the literal list of representatives.
\item Section~\ref{sec:ak50}: Lemma~\ref{lem:dominant} at $(1,2,40)$, in the form that the signed sums do not vanish; the hypotheses of Lemma~\ref{lem:goodred} in Lemma~\ref{lem:d88comp}(a): that $G$ lies in the ideal and that its coefficients are units, by evaluation in the kernel, and that the initial forms have no common zero in the torus for all weight vectors with values in any ordered abelian group, from the covering of the space of weights by polyhedral cells, checked by the kernel, with the system of each cell ruled out by cofactors checked by the kernel, except for the cell of $S_{12}$ along which the $Y$-positions escape, where a trace of the Buchberger algorithm gives a chain of $2{,}044$ identities over earlier polynomials, which the kernel checks; the boxes of Lemma~\ref{lem:d88comp}(c) and~(d), with $X_l\ne0$ on each box, checked by the kernel.
\item Section~\ref{sec:ak50}, the upper bounds in Lemma~\ref{lem:d88comp}(b): an F4 algorithm written in Lean was run modulo $65521$ on $S_{12}(\mu_0)$ and on $\mathrm{KC}'(\mu_0)$, and the traces of the runs were pruned to what the final polynomials need. Each new polynomial of a trace comes with a combination of monomial multiples of earlier polynomials, and the kernel checks that the two are equal. The inputs of each trace are, up to scalars, the polynomials of its system, as the kernel also checks. So the final polynomials of the first trace lie in $\langle S_{12}(\mu_0)\rangle$, and those of the second in $\langle\mathrm{KC}'(\mu_0)\rangle$. The kernel then checks that their leading monomials leave $20{,}316$ standard monomials for $S_{12}$ and $4788$ for $\mathrm{KC}'$.
\item Section~\ref{sec:k4}: the computation at $(3,5,7,11)$ after Proposition~\ref{prop:E4}, a Macaulay check arranged for the kernel, and Lemma~\ref{lem:C4cert} over $\F_{32003}$, from cofactor certificates with $17{,}721{,}624$ terms on the $14$ charts, checked by the kernel.
\end{itemize}

The certificate projects also contain checks of the same computations by compiled code, among them Lemma~\ref{lem:C4cert} over both primes, and they check computations of our proofs outside the formal proof. A replica of the search of Proposition~\ref{prop:cells} in Lean writes exactly the $191$ stored lists of cells, with a certificate accepted by Lemma~\ref{lem:farkas} for each of the $76{,}087{,}734$ prunes and an exact rational point in each listed cell. Each stored cell has an identity with a single term of least exponent, has a core, or is one of the $43$. Also checked are the counts of diagrams for four and five bodies and the comparison with the $117$ diagrams of \cite{CC23}, the census of Proposition~\ref{prop:cliquecount}, Lemma~\ref{lem:three} and its check at three mass points, the check of Lemma~\ref{lem:dominant} at $(1,2,7)$, the value $P_{93}(1,2,7)\ne0$ in Theorem~\ref{thm:d93}, the counts at the end of \S\ref{ss:d88}, Lemma~\ref{lem:E4cert}, Remark~\ref{rem:BEsums} and the computation at $(1,1,1,1)$ in \S\ref{ss:k4diagrams}. So are algebraic identities and finite computations inside the proofs by hand in Sections~\ref{sec:setup}--\ref{sec:cells}, \ref{sec:ak50}, \ref{sec:k4} and~\ref{sec:hand}, as lemmas over rings and fields. Of these, only the counts of patterns and tournaments and the resultants $\Res_t(R_1,R_2')$ inside the proof of Lemma~\ref{lem:E4cert} use \texttt{native\_decide}. In these checks the Lean functions are written from the definitions of the paper, without a bridge to the framework.

The formalization omits Section~\ref{sec:hand} and the treatment of diagrams $81$, $82$ and $90$ in Section~\ref{sec:ak50}.\footnote{Neither checked in Lean nor used in the proof of Theorem~\ref{thm:main} are the counts of Proposition~\ref{prop:handcover} and the checks in its proof, the comparison of the other $74$ classes with the further rules of \cite{CC23} and with the triangle rule in Section~\ref{sec:diagrams}, the kinds of prune certificates and the slacks in Table~\ref{tab:verif}, the number of decisions on argmin sets and the checks other than those in Lean in the rows of Proposition~\ref{prop:exclusion} of that table, the factorization of $P_{93}$ and its comparison with \cite{AK12}, the eliminations in the check of Lemma~\ref{lem:three} (whose results the Lean check compares with $S_\mu$), the numbers of cones in Lemma~\ref{lem:d88comp}(a), the direct test of the signed sums at $(1,2,7)$, and the correspondence with the shapes S1--S8 of \cite{AK12}.}