\section{Lexicographic separation}\label{sec:lex}

Let $m\in(\R_{>0})^5$, and let $C\subseteq Y_m$ be a nontrivial curve. By \eqref{eq:balx} the types of the singular places of $C$ satisfy $\sum_Pd_P\,x(P)=0$ with $d_P>0$, and at least one place is singular. By Theorem~\ref{thm:types} each type lies in the attained set of a piece of $\mathrm{pieces}(S(m))$. Thus $m$ is settled as soon as $0$ is not a positive combination of points of these attained sets.

\subsection{The separation lemma}\label{ss:lexlemma}

\begin{lemma}\label{lem:lex}
Let $G_1,\dots,G_M$ be finite subsets of $\Q^{10}$, let $l_1,\dots,l_r\in\Q^{10}$, and let $I_1\cup\dots\cup I_r=\{1,\dots,M\}$ be a partition such that for every $i$:
\begin{enumerate}[label=\textup{(\roman*)}]
\item $l_i\cdot v\ge0$ for every $v\in G_j$ and every $j\in I_i\cup I_{i+1}\cup\dots\cup I_r$;
\item for every $j\in I_i$ there is $v\in G_j$ with $l_i\cdot v>0$.
\end{enumerate}
Then $0$ is not a positive combination of $N\ge1$ points of $\bigcup_j\relint\conv(G_j)$.
\end{lemma}

\begin{proof}
Suppose that $0=\sum_{s=1}^N\lambda_sx_s$ with $N\ge1$, $\lambda_s>0$ and $x_s\in\relint\conv(G_{j(s)})$, and let $i$ be the least index such that $j(s)\in I_i$ for some $s$. Each $x_s$ is a convex combination of points of $G_{j(s)}$ with $j(s)\in I_i\cup\dots\cup I_r$. So $l_i\cdot x_s\ge0$ by (i). A point $x$ of $\relint\conv(G)$ is a convex combination of all points of $G$ with positive weights: if $b$ is the barycentre of $G$ and $\delta>0$ is so small that $x+\delta(x-b)\in\conv(G)$, then $x=(1+\delta)^{-1}\big(x+\delta(x-b)\big)+\delta(1+\delta)^{-1}b$. Hence (ii) gives $l_i\cdot x_s>0$ whenever $j(s)\in I_i$. There is such an $s$. Therefore we obtain $0=l_i\cdot\sum_s\lambda_sx_s>0$, a contradiction.
\end{proof}

The functionals act in stages. The first is nonnegative on all sets and positive somewhere on each set of $I_1$. Hence no point of these sets can occur in a vanishing positive combination. The second does the same among the remaining sets, and so on. Listing more sets $G_j$ can only make the hypotheses harder to satisfy.

\subsection{Certificates}\label{ss:certs}

A \emph{D5 hull} is a finite union of polytopes in the five coordinates of \S\ref{ss:d5}, such as $\Vtwo^{\mathrm w}$. Its attained faces enter $\mathrm{pieces}(S)$ as in Definition~\ref{def:piece}.

\begin{definition}\label{def:cert}
Let $S$ be a set of labels and $V$ a D5 hull. Let $\cA_V(S)$ be the list of the attained faces of the pieces of $\mathrm{pieces}(S)$ (Definition~\ref{def:piece}), with the attained faces of $V$ in place of those of $\Vtwo^{\mathrm w}$. We record each face by the finite set of its vertices. A \emph{certificate} for $S$ relative to $V$ is a finite sequence $l_1,\dots,l_r\in\Z^{10}$ such that
\begin{enumerate}[label=\textup{(\alph*)}]
\item for each $i$, $l_i\cdot v\ge0$ for every vertex $v$ of every face of $\cA_V(S)$ on whose vertices $l_1,\dots,l_{i-1}$ all vanish, and
\item every face of $\cA_V(S)$ has a vertex $v$ with $l_i\cdot v>0$ for some $i$.
\end{enumerate}
A set $S$ is \emph{certified} relative to $V$ if it has a certificate relative to $V$.
\end{definition}

Let $I_i$ be the set of faces on whose vertices $l_1,\dots,l_{i-1}$ vanish and $l_i$ is positive at some vertex. By induction on $i$, (a) and (b) say that the sets $I_i$ partition $\cA_V(S)$ and satisfy (i) and (ii) of Lemma~\ref{lem:lex}. Since $\mathrm{pieces}(S)$ grows with $S$ and the attained faces of a piece do not depend on $S$, a certificate for $S$ is a certificate for every $S'$ with $\mathrm{pieces}(S')\subseteq\mathrm{pieces}(S)$, in particular for any subset of $S$.

\begin{definition}\label{def:validhull}
A D5 hull $V$ is \emph{valid} at $m\in(\R_{>0})^5$ if the conclusion of Theorem~\ref{thm:types} holds at $m$ with $V$ in place of $\Vtwo^{\mathrm w}$.
\end{definition}

\begin{proposition}\label{prop:cert}
Let $m\in(\R_{>0})^5$, let $V$ be a D5 hull valid at $m$, and let $S$ be a set of labels with $\mathrm{pieces}(S(m))\subseteq\mathrm{pieces}(S)$, for instance $S\supseteq S(m)$. If $S$ is certified relative to $V$, then $m$ is settled.
\end{proposition}

\begin{proof}
Let $C\subseteq Y_m$ be a nontrivial curve. By \eqref{eq:balx} we have $\sum_Pd_Px(P)=0$, with $d_P>0$ and at least one singular place $P$. By Theorem~\ref{thm:types} and the validity of $V$, each $x(P)$ lies in the relative interior of an attained face of some piece in $\mathrm{pieces}(S(m))$, built with $V$. This face belongs to $\cA_V(S)$. A face and the convex hull of its vertices have the same relative interior. Thus $0$ is a positive combination of points of $\bigcup_{G\in\cA_V(S)}\relint\conv(G)$, which is excluded by Lemma~\ref{lem:lex}, applied with the partition $(I_i)$ of the certificate. Hence no such curve exists.
\end{proof}

The pieces $\pc{d2}[T]$, $\pc{d9}(T;ax,by)$, $\pc{d14a}$, $\pc{d14b}$ and $\pc{d15}$ are present for every label set. Proposition~\ref{prop:nod2}, Theorem~\ref{thm:D9}, Corollary~\ref{cor:nod15} and Theorem~\ref{thm:D14} remove the pieces $\pc{d2}[T]$, $\pc{d9}(T;ax,by)$, $\pc{d15}(j,k)$ and $\pc{d14b}(j,k)$, respectively, at all positive masses, so that for every label set $S$ we may leave the attained faces of these pieces out of $\cA_V(S)$. By Corollary~\ref{cor:Kdrop} we may remove the pieces $\pc{d14a}(j)$ when $\mathrm{K14}(m_{Q_j})$ has no solution. Hence, if $\mathrm{K14}(m_{Q_j})$ has no solution for every body $j$ of a set $J$, we may leave the attained faces of $\pc{d14a}(j)$, $\pc{d14b}(j,k)$ and $\pc{d15}(j,k)$, $j\in J$, $k\in Q_j$, out of $\cA_V(S)$, and the proof of Proposition~\ref{prop:cert} applies to the remaining faces. We call the verification of (a) and (b) for these faces the \emph{final check} of $(S,J)$. The resulting notion of a K-certified point is Definition~\ref{def:Kcert}. Proposition~\ref{prop:Kcert} states that a K-certified point is settled.

\subsection{Exact verification}\label{ss:lexexact}

All vertices of the pieces of Table~\ref{tab:pieces}, with the cells of Table~\ref{tab:d7}, and all vertices of the polytopes of the D5 hulls used below have rational coordinates whose denominators divide $168$. We check a certificate in integer arithmetic, after multiplying the vertices by $168$ and asserting that every vertex becomes integral. We do not take the face list from the certificate: we recompute it from the label set $S$ and the pieces that the certificate leaves out. That is, we
\begin{enumerate}[label=(\arabic*)]
\item enumerate the pieces enabled by $S$, with an exact implementation of Tables~\ref{tab:pieces} and~\ref{tab:d7}, without the pieces $\pc{d2}[T]$ and $\pc{d9}(T;ax,by)$;
\item check that each polygon is strictly convex, with its vertices in the given cyclic order;
\item compute the face lattice of each polytope of the hull exactly, and embed the attained faces for each $\lab{E}(T)$ implied by $S$;
\item remove the pieces that the certificate leaves out, among them those of the clusters named in a final check; and
\item evaluate each $l_i$ at every vertex.
\end{enumerate}
The list so built is the list that the certificate must separate, which leaves out the faces of all pieces $\pc{d2}$ and $\pc{d9}$ (\S\ref{ss:certs}). We will check all certificates in \S\S\ref{sec:points}--\ref{sec:curves} this way.

We find the functionals by solving, stage by stage, a linear program in floating point (HiGHS) on the faces not yet separated, and rationalizing its solution. We accept a stage only if the exact check accepts it.

\begin{remark}\label{rem:hulls}
We use three D5 hulls of \S\ref{ss:d5}:
\begin{enumerate}[label=(\roman*)]
\item $\Vtwo^{\mathrm w}$, valid at all positive masses;
\item $\Vtwo\subseteq\Vtwo^{\mathrm w}$, valid when $m_o\ne m_a+m_b$ for every $o$ in each triangle $T=\{o,a,b\}$ with $\lab{E}(T)\in S(m)$;
\item $\VN\subseteq\Vtwo$, valid at the mass points described in \S\ref{ss:d5}.
\end{enumerate}
Each of them contains the projection of its model (Theorem~\ref{thm:hulls} and Lemma~\ref{lem:infty}). We apply each certificate below that uses $\VN$ only where $\VN$ is valid (checked in \S\ref{sec:verification}).
\end{remark}

\subsection{Certificates for the mass conditions}\label{ss:masscert}

To apply Proposition~\ref{prop:cert} on a set of masses we have to know which labels can hold there. We make these decisions by the kinds of certificate listed below. Each is \emph{rigorous}: it may fail to decide, but a decision it returns is correct, given the enclosure property of ball arithmetic (Arb, through python-flint~0.9.0) and the correctness of exact integer, rational and polynomial arithmetic. Search parameters (the degree bound of the filter (F2) of \S\ref{ss:flats}, initial grids, depth and time limits, working precisions, Krawczyk preconditioners and the tie-breaking constants of \S\ref{sec:rays}) and floating-point proposals, such as the solutions of the linear programs, affect only running time, the numbers of flats and boxes, and whether a search succeeds: all acceptances and exclusions are decided by rigorous enclosures or exact checks. Hence a wrong proposal can only make a search fail.

\begin{enumerate}[label=\textup{(C\arabic*)},leftmargin=*]
\item \emph{Exact computer algebra.} Standard bases, minimal primes and saturations of ideals of polynomials over $\Q$. With them we describe the points of a stratum of the sorted masses at which given labels hold. The details are in \S\ref{ss:flats}.
\item \emph{Exact algebraic decisions.} Feasibility of linear systems over $\Q$ (Fourier--Motzkin elimination), polynomial identities, arithmetic in number fields $\Q[\theta]/(f)$, and real root isolation over $\Q$ by Sturm sequences or Descartes' rule of signs.
\item \emph{Point certificates.} At an exact mass point, we show by the certificates of \S\ref{sec:points} that the system $\mathrm{K14}$ of a cluster has no solution.
\end{enumerate}

A label set certified in the sense of Definition~\ref{def:cert} is a statement about pieces only. The classes (C1)--(C3) connect it to the masses:
\begin{enumerate}[label=(\roman*)]
\item by (C1) and (C2), the label set of every positive mass vector with $m_1\le\dots\le m_5$ is certified in the sense of \S\ref{ss:nearlabels}, contains a curve set, or is that of one of two exact points (Theorem~\ref{thm:S});
\item the mass vectors whose label set contains a curve set lie, up to scaling and relabelling, on the curve families (Lemma~\ref{lem:DT}), which we treat with (C2) and (C3) in \S\ref{sec:curves} and by counting in \S\ref{sec:rays};
\item at the two exact points the hull $\VN$ certifies the label set (Proposition~\ref{prop:Spoints}).
\end{enumerate}
We describe in \S\ref{ss:checks} how these computations are checked.