\documentclass[11pt]{amsart} \usepackage[margin=1.1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{graphicx,booktabs,enumitem,array} \usepackage[hidelinks]{hyperref} \hypersetup{pdftitle={The number of planar central configurations of four bodies}, pdfauthor={Tejasvi Singh Tomar}} \newtheorem{mainthm}{Theorem} \newtheorem{lemma}{Lemma}[section] \newtheorem{theorem}[lemma]{Theorem} \newtheorem{proposition}[lemma]{Proposition} \newtheorem{corollary}[lemma]{Corollary} \theoremstyle{definition} \newtheorem{definition}[lemma]{Definition} \theoremstyle{remark} \newtheorem{remark}[lemma]{Remark} \newtheorem*{remark*}{Remark} \numberwithin{equation}{section} \setlength{\emergencystretch}{2em} \DeclareTextSymbolDefault{\textsection}{OMS}% the section sign from cmsy (Type 1), not from a bitmap TS1 font \makeatletter\edef\ttus@fam{\ttdefault}\DeclareRobustCommand{\_}{\ifmmode\nfss@text{\textunderscore}\else\edef\ttus@cur{\f@family}\ifx\ttus@cur\ttus@fam\char95\relax\else\textunderscore\fi\fi}\makeatother% typewriter underscores as the cmtt glyph, so that names copy with their underscores \newcommand{\R}{\mathbb{R}} \newcommand{\Om}{\Omega_4} \newcommand{\cD}{\mathcal{D}} \newcommand{\Db}{\overline{\mathcal{D}}} \newcommand{\cU}{\mathcal{U}} \newcommand{\Sym}{\mathfrak{S}_3} \newcommand{\sB}{s_{\mathrm{lo}}} \newcommand{\sH}{s_{\mathrm{hi}}} \newcommand{\rtop}{r_{\mathrm{top}}} \newcommand{\rax}{r_{\mathrm{ax}}} \newcommand{\rhtop}{\hat r_{\mathrm{top}}} \newcommand{\Tfin}{T_{\mathrm{fin}}} \newcommand{\lax}{\lambda_{\mathrm{ax}}} \newcommand{\hA}{\widehat A} \newcommand{\Av}{\mathbf{A}} \newcommand{\hv}{\mathbf{h}} \newcommand{\Jt}{\widetilde J} \newcommand{\Jm}{J_{\mathrm{mir}}} \DeclareMathOperator{\atantwo}{atan2} \begin{document} \title{The number of planar central configurations of four bodies} \author{Tejasvi Singh Tomar} \address{Independent researcher} \renewcommand{\urladdrname}{{\itshape ORCID}} \urladdr{\href{https://orcid.org/0000-0003-4668-3639}{https://orcid.org/0000-0003-4668-3639}} \subjclass[2020]{70F10, 70F15, 55M25, 58K05, 65G40} \keywords{Central configurations, four-body problem, relative equilibria, Dziobek configurations, mapping degree, Whitney cusp, computer-assisted proof, interval arithmetic} \begin{abstract} For four positive masses in the plane we determine the number $N$ of central configurations, counted up to rotation, translation and scaling, in terms of one fold surface, whose certified enclosures decide $N$ for all masses outside a closed null set. Of these configurations, $12$ are collinear, by Moulton's theorem, and $6$ are convex, by the existence theorem of MacMillan and Bartky and the uniqueness proved in the author's preprint arXiv:2609.35632. Through Dziobek's relations, the concave configurations with inner body $i$ form the fibre of a proper mass map of degree $2$. Their number $c_i$, counted up to reflection, is $1$, $2$, $3$ or $4$, and we read it off from the position of the mass ratios relative to this surface. Altogether $N=18+2(c_1+c_2+c_3+c_4)$, an even number with $32\le N\le50$. Moreover $N=32$ exactly at Palmore's masses, and every even value in this range occurs. For four equal masses we recover Albouy's count $N=50$. The proof shows with interval certificates that the mass map is injective where its Jacobian is not positive, obtains its degree from the restricted problem, and analyses its folds, cusps and Palmore's umbilic. A formalization in Lean also proves these results. \end{abstract} \maketitle \section{Introduction}\label{sec:intro} \subsection{Central configurations of four bodies}\label{sec:ccs} Consider four bodies with masses $m_1,\dots,m_4>0$ at positions $x_1,\dots,x_4\in\R^2$. We write $r_{ij}=|x_i-x_j|$, $M=\sum_im_i$ and $c_m=M^{-1}\sum_im_ix_i$. A collision-free configuration $x=(x_1,\dots,x_4)$ is a \emph{central configuration} (CC) if \begin{equation}\label{eq:cc} \sum_{i\ne j}m_i\,\frac{x_i-x_j}{r_{ij}^{3}}=-\lambda\,(x_j-c_m),\qquad j=1,\dots,4, \end{equation} for some $\lambda\in\R$. The planar CCs are the configurations of the relative equilibria, the solutions of the Newtonian four-body problem that rotate rigidly about their centre of mass. A non-collinear configuration is \emph{convex} if the four bodies are the vertices of a strictly convex quadrilateral. It is \emph{concave} if one body lies strictly inside the triangle of the other three. Each non-collinear CC is of one of these two types: by the perpendicular bisector theorem \cite{Moe90}, no four-body CC has exactly three bodies collinear \cite[\S2.2]{HM06}. We count CCs modulo similarity in two ways that differ in the treatment of mirror images. \begin{itemize}[leftmargin=2em] \item $N(m)$ is the number of planar CCs up to rotation, translation and scaling. A configuration and its mirror image count separately. In this convention, used in \cite{Mou10,Sim78,HM06}, the collinear CCs form $4!/2=12$ classes. \item $c_i(m)$ is the number of concave CCs with body $i$ strictly inside the triangle of the other three. It counts up to similarity including reflection: a configuration and its mirror image count once. \end{itemize} Since an orientation-reversing similarity fixes no three non-collinear points, a non-collinear CC is never equivalent, as a labelled configuration, to its mirror image under rotations, translations and scalings. Each class counted by $c_i(m)$ therefore consists of two classes in $N(m)$. Whether the number of central configurations is finite for all positive masses is a question of Chazy \cite{Cha18} and Wintner \cite{Win41}. Smale listed it as the sixth of his problems for this century \cite{Sma98} (see also \cite[Problem~9]{ACS12}). For five bodies in the plane, Albouy and Kaloshin \cite{AK12} proved finiteness except perhaps for masses in an explicit subvariety of codimension~$2$. For four bodies, Moeckel \cite{Moe01} proved finiteness for almost all masses. Hampton and Moeckel \cite{HM06} proved that $N(m)$ is finite for all positive masses and that $32\le N(m)\le8472$. Simó's numerical experiments \cite{Sim78} suggest that $32\le N(m)\le50$. Figueras, Tucker and Zgliczyński \cite{FTZ24} named the unrestricted four-body problem as their next challenge, expecting between $32$ and $50$ relative equilibria. We determine $N(m)$ for every positive mass vector in terms of one function $R$ (Theorems~\ref{thm:count} and~\ref{thm:N}), whose certified enclosures decide $N(m)$ for all $m$ outside a closed null set (Remark~\ref{rem:effective}). In particular, the range suggested by Simó's experiments holds for all masses, and every even value in it occurs. The bound $8472$ of \cite{HM06} comes from a count of complex solutions: the mixed volume of a system of ten polynomial equations bounds their number, at most one third of them have real mutual distances, and adding the $12$ collinear CCs to that third gives $8472$ \cite[\S6.2]{HM06}. We count real configurations directly. The concave CCs with a given inner body are the preimages of a proper map of degree $2$, of which at most one has negative Jacobian. At the critical values a local analysis of the map determines their number (Section~\ref{sec:idea}). Adding the $12$ collinear and the $6$ convex CCs, we obtain $N=12+6+2\sum_ic_i$. The term $12$ of this count is Moulton's theorem \cite{Mou10} that there are exactly $12$ collinear CCs for any choice of masses. For the term $6$, MacMillan and Bartky \cite{MB32} proved that each of the three cyclic orders of the bodies is realized by a convex CC (a simpler proof is in \cite{Xia04}). Albouy, Fu and Sun conjectured that this convex CC is unique up to similarity for all masses \cite{AFS08}. This was known when the two ends of a diagonal carry equal masses \cite{Lea03,AFS08}. It is Problem~10 in the list of open problems of Albouy, Cabral and Santos \cite{ACS12}. The author proved it for all cyclic orders and all positive masses in the preprint \cite{Tom26}, where the proof, including its computer-assisted part, is also formalized in Lean. Albouy \cite{Alb95,Alb96} determined the CCs of four equal masses (see also \cite[\S1]{CCLM15}): there are $50$ of them \cite[\S6.1]{HM06}. For the masses $(1,1,1,m_4)$, Rusu and Santoprete \cite{RS16} computed the CCs numerically and established the fold and pitchfork bifurcations with interval methods. Their table lists the numbers $D$ of solutions of the Dziobek equations. Since these equations are written in the mutual distances, their solutions are the non-collinear CCs up to similarity including reflection. With the $12$ collinear CCs this means $N=12+2D$. In the table of Rusu and Santoprete, $N$ takes the values $32$, $38$, $44$ and $50$. Theorem~\ref{thm:N}(e) shows that the table holds exactly. Liu, Poudel, Raut and Xie \cite{LPRX26} classified the concave kite CCs of these masses by a computer-assisted proof and treated the asymmetric ones numerically. For body~$4$ inside, their classification rederives a result of Shi and Xie \cite{SX10}. For each $m_4$ the equilateral triangle with body $4$ at its centre is a CC of these masses. Palmore found that it is degenerate for $m_4=m^*=(81+64\sqrt3)/249$ \cite{PalT,PalII}. Meyer and Schmidt \cite{MS88} showed that families of isosceles CCs bifurcate from it. For concave kites, whose two off-axis bodies have equal masses, Roberts observed numerically that the mass map on kite configurations is two-to-one \cite[\S6.2 (arXiv version)]{Rob24}. In Section~\ref{sec:checks} we also compare our results with two limits of the masses. When the mass of the inner body tends to zero, the limit is the planar restricted four-body problem with equilateral primaries. It has $8$, $9$ or $10$ relative equilibria \cite{BL14} (see also \cite{Bar08,BL11}). Figueras, Tucker and Zgliczyński \cite{FTZ24} gave a computer-aided proof of this count. The limit in which the masses of the three outer bodies tend to zero is studied in \cite{CCLM15}. Among other computer-assisted counts of CCs, all CCs of $5$, $6$ and $7$ equal masses in the plane are listed in \cite{MZ19} (see also \cite{LS09}). \subsection{Results}\label{sec:results} For each body $i$ we define in Section~\ref{sec:setup} a mass map $F_i$ from an open set of spoke lengths to $\R^3$, whose fibre over the point $\mu^{(i)}(m)$ consists of the concave CCs with body $i$ inside. After relabelling the bodies so that $i=4$, \[ \mu^{(4)}(m)=\Bigl(\log\frac{m_1}{m_4},\ \log\frac{m_2}{m_4},\ \log\frac{m_3}{m_4}\Bigr). \] For another body $i$ and an order $(j_1,j_2,j_3)$ of the other three, $\mu^{(i)}(m)$ is defined in the same way and has the components $\log(m_{j_k}/m_i)$. On $\R^3$ we use the coordinates \begin{equation}\label{eq:APQ} A=\tfrac13(\mu_1+\mu_2+\mu_3),\qquad (P,Q)=\Bigl(\frac{\mu_1-\mu_2}{\sqrt2},\ \frac{\mu_1+\mu_2-2\mu_3}{\sqrt6}\Bigr)=\rho\,(\cos\Theta,\sin\Theta), \end{equation} with $\rho\ge0$ and $\Theta$ in the circle $S^1=\R/360^\circ$. We call the coordinates $(A,\rho,\Theta)$ of $\mu^{(i)}(m)$ the \emph{mass coordinates} of body $i$. In terms of the masses, $A=\log\bigl((m_{j_1}m_{j_2}m_{j_3})^{1/3}/m_i\bigr)$; the radius $\rho$ is the distance from the point $(\log m_{j_1},\log m_{j_2},\log m_{j_3})$ to the line spanned by $(1,1,1)$. Another order of the outer bodies leaves $A$ and $\rho$ unchanged and changes $\Theta$ by an element of the dihedral group $D_3$ generated by $\Theta\mapsto\Theta+120^\circ$ and $\Theta\mapsto180^\circ-\Theta$. The radius $\rho$ vanishes exactly when the three outer masses are equal. For $\rho>0$, $\Theta\in\{90^\circ,210^\circ,330^\circ\}$ exactly when two outer masses are equal and the third is smaller, and $\Theta\in\{30^\circ,150^\circ,270^\circ\}$ exactly when two outer masses are equal and the third is larger. Let $m^*=(81+64\sqrt3)/249$ be Palmore's mass ratio and $A^*=-\log m^*$. Then $(A,\rho)=(A^*,0)$ exactly when the three outer masses are equal to some $m_0$ and $m_i=m^*m_0$. We then call $m$ a \emph{Palmore mass vector}. \begin{mainthm}\label{thm:count} There is a continuous function $R:\R\times S^1\to[0,\infty)$, invariant under $D_3$ in its second argument, with $R(A,\Theta)=0$ if and only if $A=A^*$, such that the following holds. For every positive mass vector $m$ and every body $i$, the number $c_i(m)$ is given by Table~\ref{tab:count} in terms of the mass coordinates $(A,\rho,\Theta)$ of body $i$. The critical values of $F_i$ are exactly the points of $\R^3$ with $\rho=R(A,\Theta)$. \end{mainthm} \begin{table}[ht] \centering\small \begin{tabular}{@{}lc@{}} \toprule mass coordinates $(A,\rho,\Theta)$ of body $i$ & $c_i(m)$\\ \midrule $\rhoR(A,\Theta)$ & $2$\\ $\rho=R(A,\Theta)$, $A\ne A^*$, $\Theta\in\{90^\circ,210^\circ,330^\circ\}$ (cuspidal edge) & $2$\\ $\rho=R(A,\Theta)$, $A\ne A^*$, $\Theta\notin\{90^\circ,210^\circ,330^\circ\}$ (fold sheet) & $3$\\ $A=A^*$, $\rho=0$ (Palmore mass vector) & $1$\\ \bottomrule \end{tabular} \par\vspace{6pt} \caption{The number $c_i(m)$ of concave CCs with body $i$ inside (Theorem~\ref{thm:count}).}\label{tab:count} \end{table} For $A\ne A^*$, the critical values of $F_i$ at the level $A$ form the star-shaped curve $\rho=R(A,\Theta)$ around the axis $\rho=0$. Each of them has exactly one critical point in its fibre (Section~\ref{sec:surface}). In this way one surface in $\R^3$, the same for the four bodies, determines all the numbers $c_i(m)$. Figure~\ref{fig:surface} shows it on the rays $\Theta=90^\circ$ and $\Theta=270^\circ$. Let $Z_i$ be the set of masses $m\in(0,\infty)^4$ for which $\mu^{(i)}(m)$ is a critical value of $F_i$. Each $Z_i$ is a closed null set (Proposition~\ref{prop:regcount} and Section~\ref{sec:proofN}). \begin{figure}[t] \centering \includegraphics[width=\textwidth]{fig_surface.pdf} \caption{The surface of critical values $\rho=R(A,\Theta)$ of Theorem~\ref{thm:count} on the mirror rays $\Theta=90^\circ$ (cuspidal edge) and $\Theta=270^\circ$ (fold sheet), at $32$ levels of $A$ from $A^*-1.75$ to $A^*+3.5$, against $A$, with $R$ on a logarithmic axis (a), and against $|A-A^*|$ on logarithmic axes (b). The marks are circles on the ray $\Theta=90^\circ$ and squares on the ray $\Theta=270^\circ$. In (b) they are filled on the lower nappe ($A>A^*$) and open on the upper nappe ($A0$, $N=38$ for $m_4\in(0,m^*)\cup(m^*,m^{**}]\cup(m_f,\infty)$, $N=32$ for $m_4=m^*$, $N=50$ for $m_4\in(m^{**},m_f)$ and $N=44$ for $m_4=m_f$, where $m^{**}=0.99184227439\ldots$ and $m_f=1.00266054757\ldots$ are defined in Section~\ref{sec:family}. The masses $(1,1,1,m_4)$ lie in $Z_1\cup Z_2\cup Z_3\cup Z_4$ exactly for $m_4\in\{m^*,m^{**},m_f\}$. \item A concave CC is degenerate, in the sense recalled in Section~\ref{sec:degenerate}, if and only if the Jacobian of the mass map of its inner body vanishes there. Every degenerate concave CC has nullity $1$, except, for each Palmore mass vector, the equilateral triangle of the three equal masses with the fourth body at its centre, which has nullity $2$. In the coordinates given by the spoke lengths (Lemma~\ref{lem:dziobek}), the degenerate concave CCs with a given inner body form a set homeomorphic to a double cone. \item $N(1,1,1,1)=50$. \end{enumerate} \end{mainthm} Theorem~\ref{thm:N} follows from Theorem~\ref{thm:count} with the collinear and convex counts of Section~\ref{sec:ccs}, certified computations of $R$ at exact masses (Section~\ref{sec:examples}), the exact treatment of the family $(1,1,1,m_4)$ in Section~\ref{sec:family} and a lemma on degeneracy (Section~\ref{sec:degenerate}). Section~\ref{sec:proofN} contains the details. Through the convex count, the formula for $N$ uses the uniqueness theorem of \cite{Tom26}. Without it the same argument gives $N\ge18+2\sum_ic_i$, because the existence theorem provides at least $6$ convex CCs, and $N$ is still even, because convex CCs come in mirror pairs. For the masses $(1,1,1,m_4)$ each cyclic order has a diagonal whose ends carry equal masses, where uniqueness was known \cite{Lea03,AFS08}. Hence the formula for general masses, the bound $N\le50$ in (a) and items (c) and (d) depend on \cite{Tom26}; the other items and Theorem~\ref{thm:count} do not. Items (a) and (b) show that the lower bound $32$ of \cite{HM06} is sharp and is attained exactly at the Palmore mass vectors. Item (e) is the table of Rusu and Santoprete \cite{RS16}. The values $32$ and $44$ of that table occur at critical values. For $m=(1,1,1,m^*)$ the point $\mu^{(4)}(m)$ is the vertex $(A^*,0)$ of the surface and $c_4=1$. For $m=(1,1,1,m_f)$ the point $\mu^{(1)}(m)$ lies on a fold sheet and $c_1=c_2=c_3=3$. Item (g) is Albouy's count. For four equal masses the $32$ concave CCs are the $8$ equilateral configurations with a body at the centre and $24$ isosceles ones (Theorem~\ref{thm:count} and Proposition~\ref{prop:cert}(g)). That $c_i(m)\ge1$ for all $i$ and $m$ was known: by Hampton's theorem \cite{Ham02} (see \cite[\S6.1]{HM06}), for all positive masses there is a concave CC with any given body inside. Theorem~\ref{thm:count} also makes the count effective. Off the surface of critical values the sign of $\rho-R(A,\Theta)$ decides $c_i(m)$. An interval enclosure of $R(A,\Theta)$ can be computed by an interval Newton step at a single point of the fold, without a search for other zeros (Remark~\ref{rem:effective}). Section~\ref{sec:examples} will use this to certify $N$ at exactly given masses. \subsection{The idea of the proof}\label{sec:idea} Label the inner body $4$. A concave CC with body $4$ inside, scaled so that $\lambda/M=1$, is determined up to isometry by its three spoke lengths $a_i=|x_i-x_4|$. Dziobek's relations express the masses as analytic functions of $a=(a_1,a_2,a_3)$ on an open set $\Om\subset(0,1)^3$, through the angles $\theta_i$ at body $4$ and an auxiliary quantity $K$, which $a$ determines implicitly (Lemma~\ref{lem:angles}). Then $c_4(m)$ is the number of preimages of the mass ratios under the mass map $F=F_4:\Om\to\R^3$. Let $J$ be its Jacobian determinant, $\cD=\{J<0\}$, $\Db=\{J\le0\}$ and $\Sigma=\{J=0\}$, the \emph{fold}. In the coordinates \eqref{eq:APQ} on the target we write $F=(A,G)$ with $G=(P,Q)$. We proceed in six steps, of which step (2) is the main difficulty. Injectivity is a global property, whereas the fold has no closed form away from the axis and interval certificates check only local inequalities. Slicing by the levels of $A$ turns it into statements about the angle of $G$ along the fold curves $\Gamma_c$, which sign conditions at the points of the fold can certify. \begin{enumerate}[label=(\arabic*),leftmargin=2em] \item \emph{The axis.} The symmetric group $\Sym$ permutes the outer bodies. It acts in the same way on the plane orthogonal to the axis $a_1=a_2=a_3$ and on the plane of $G$. On the axis this reduces $dF$, in coordinates adapted to the axis, to a diagonal matrix with entries $\partial_sA$, $\lax$, $\lax$, so that $J=\partial_sA\cdot\lax^2$ on the axis (Lemma~\ref{lem:axis}). Both factors have closed forms (Proposition~\ref{prop:ax}). These closed forms show that $\partial_sA<0$ and that $\lax$ has exactly one zero $s^*$, at which the mass ratio is Palmore's value $m^*$. The Jacobian is negative on the axis except at Palmore's configuration $p^*=s^*(1,1,1)$, the \emph{umbilic}, where $dF$ has rank one. \item \emph{Injectivity on $\Db$.} We prove that $F$ is injective on $\Db$ (Sections~\ref{sec:rays}--\ref{sec:injective}). Corbera, Cors and Roberts proposed the same strategy for convex CCs: to prove their uniqueness by showing that a suitably normalized mass map is injective \cite{CCR19}. Interval certificates, together with the lemmas of Section~\ref{sec:hand}, show that $\Db$ lies in an explicit neighbourhood of the axis, the fold core, and meets every ray from the axis in an initial segment. Since $\Db$ meets the plane $s=s^*$ only at $p^*$ (Proposition~\ref{prop:cert}(e)), the umbilic splits $\Db$ into two nappes. On each nappe $A$ is a proper map onto a half-line. The level sets $\Phi_c$ of $A$ on a nappe are bounded by curves $\Gamma_c$ on the fold. Each $\Gamma_c$ meets each half-plane bounded by the axis exactly once. Along $\Gamma_c$ the angle of $G$ is monotone, by certified sign conditions. It makes exactly one turn, by the symmetry and a certified half-plane condition. The image of $\Gamma_c$ under $G$ is then a star-shaped curve $C_c$ (Figure~\ref{fig:curves}). Over the region bounded by $C_c$ the map $G|_{\Phi_c}$ is a covering. A count at one point near the fold shows that it has one sheet. So $G$ maps $\Phi_c$ homeomorphically onto the closed region bounded by $C_c$, and $\Phi_c$ is a closed disk. As $A$ separates the level sets and the two nappes, $F$ is injective on $\Db$. \item \emph{The count at regular values.} Let $n_\pm$ be the numbers of preimages of a regular value at which $\pm J>0$. Since $F$ is proper (Section~\ref{sec:proper}), $n_+$ and $n_-$ are locally constant on the regular values. Step (2) shows that the regular values form three connected sets: the values inside the surface $F(\Sigma)$ with $A>A^*$, those inside it with $A0$, $c_4(\mu)=3-k$, where $k$ is the local degree of $F$ at $q$ (Lemma~\ref{lem:localcount}). As $A$ is a local coordinate everywhere on $\Om$, we compute $k$ for the planar map $G$ on the level surface of $A$ through $q$. At a fold point, where the angle of $G$ moves along $\Gamma_c$, the normal form of step (3) shows that $k=0$ (Proposition~\ref{prop:foldcount}). On the mirrors $a_i=a_j$, where the angle of $G$ can be stationary, a $\mathbb Z/2$-equivariant normal form and a quantitative version of the band lemma show that $F$ has a cusp with $k=1$ at all cusp points, that is, at the points of the fold other than $p^*$ that lie on a mirror and at which the mirror determinant $\Jm$ of Section~\ref{sec:mirror} does not vanish (Proposition~\ref{prop:cuspcount}). At $p^*$ the map $G$ on the level $A=A^*$ is $c(s^*)\bar z^2+O(|z|^3)$, where $z=x+iy$ is a complex coordinate orthogonal to the axis. The coefficient $c(s^*)$ has a closed form and does not vanish (Proposition~\ref{prop:U}). It follows that $k=2$ (Proposition~\ref{prop:umbcount}). \item \emph{The surface of critical values.} Steps (2) and (4) show that for $c\ne A^*$ the image $F(\Db)\cap\{A=c\}$ is the closed region bounded by $C_c$, the curve $\rho=R(c,\Theta)$ of Theorem~\ref{thm:count}. A value inside $C_c$ has one preimage in $\cD$ ($c_4=4$), a value outside has none ($c_4=2$), and a value on $C_c$ has $c_4=3$ or $c_4=2$ according as it comes from a fold point or a cusp point. On each nappe the cusp points are the points of the fold on three of the six half-mirrors, which places the cuspidal edges at $\Theta\in\{90^\circ,210^\circ,330^\circ\}$ (Proposition~\ref{prop:classify}). This yields Table~\ref{tab:count} for body $4$; the other bodies follow by relabelling. \item \emph{Counting.} Theorem~\ref{thm:N} then follows as described after its statement. \end{enumerate} The interval certificates (Section~\ref{sec:cert}) provide the location of $\Db$, the transversality of the fold, the sign conditions that make the angle of $G$ monotone, the half-plane condition that fixes its total turn, and the strict bounds behind the cusps. Inside $\Om$, box-by-box sign checks cannot succeed in two places, where quantities to be signed vanish. On the mirrors the angle of $G$ is stationary at the cusps of $C_c$. Lemma~\ref{lem:band} (the band lemma) handles these points. At $p^*$, where all first derivatives of $G$ vanish, a separate chart certifies the quantities divided by powers of the distance to $p^*$ (Section~\ref{sec:balls}). The certificates are finite covers of the configuration space by boxes. Each box carries ball-arithmetic enclosures of the relevant quantities and the sign conditions derived from them. \begin{figure}[t] \centering \includegraphics[width=\textwidth]{fig_curves.pdf} \caption{The curves $C_c=G(\Gamma_c)$ for $c=\log2$ on the lower nappe (left) and $c=0$ on the upper nappe (right), computed in floating point. The dot is the origin, the image of the axis point of the disk $\Phi_c$. This point has $m_4/m=1/2$ on the left. On the right it is the equilateral configuration of four equal masses. The dashed lines are the mirror rays $\Theta=30^\circ+k\cdot60^\circ$. Each curve meets every ray from the origin once. It has cusps on the mirror rays $\Theta=90^\circ$, $210^\circ$ and $330^\circ$ and crosses the other three mirror rays transversally, as Proposition~\ref{prop:classify} shows for all levels $c\ne A^*$. The two curves look alike, but the cusp points of $\Gamma_c$ lie on the half-mirrors $\varphi\in\{90^\circ,210^\circ,330^\circ\}$ on the lower nappe and on $\varphi\in\{30^\circ,150^\circ,270^\circ\}$ on the upper nappe.}\label{fig:curves} \end{figure} \subsection{Ingredients of the proof}\label{sec:rests} The proof of Theorem~\ref{thm:count} uses Dziobek's relations (Lemma~\ref{lem:dziobek}). The proof of properness (Proposition~\ref{prop:proper}) uses the absence of CCs with exactly three bodies collinear. Theorem~\ref{thm:N} uses in addition the collinear count \cite{Mou10} and the convex count \cite{MB32,Xia04,Tom26}; the paragraph after its statement says which of its items depend on \cite{Tom26}. Neither theorem uses Albouy's count \cite{Alb95,Alb96}: we compute the degree in the limit of large $A$, not at equal masses. The computer-assisted parts of the proof are the certificates of Section~\ref{sec:cert}, used for Theorem~\ref{thm:count}, and, for Theorem~\ref{thm:N}(b), (d) and (e), the certified computations of points of the fold in Section~\ref{sec:examples} and the exact computations behind the family theorem of Section~\ref{sec:family}. The closed forms of Propositions~\ref{prop:ax} and~\ref{prop:U} are derived and checked by computer algebra in exact arithmetic. Data and code availability lists what the computations assume and which of the reported computations test the proof without being part of it. Theorems~\ref{thm:count} and~\ref{thm:N} have two proofs, and the proof of record is the one in this paper. It rests on the computations just listed, which Data and code availability describes, and most of their certified quantities come from one implementation in C. The other proof is a formalization in Lean, also described there, whose main theorem states both theorems and takes no unproved inputs; its computer-assisted steps are certificates of its own, which the Lean kernel checks. The evaluator of Section~\ref{sec:examples}, a second rigorous implementation, reproduces the values of $K$, $\hA$, $P$, $Q$, $\Jt$, $T_1$, $T_2$, $T_3$ and $\Jm$ computed by the C code, but only at $100$ points of chart~$1$ (Section~\ref{sec:exlist}). For the other quantities that the proof in this paper takes from the C code, which Data and code availability lists, the independent assurance is the formal proof, which does not depend on the C code. Data and code availability names, for each certified ingredient of Sections~\ref{sec:thm1} and~\ref{sec:critical}, its counterpart in the formalization, or why the formalization needs none. \subsection{Organization} Section~\ref{sec:setup} introduces the Dziobek reduction, the mass map, its symmetry and the axis. It also contains the closed forms on the axis and at the umbilic. Section~\ref{sec:fold} derives the formulas on the fold used in the certificates. Section~\ref{sec:hand} collects lemmas that delimit the configuration space, and Section~\ref{sec:cert} describes the certificates. In Section~\ref{sec:thm1} we prove the injectivity of $F$ on $\Db$ and the count at regular values. Section~\ref{sec:critical} computes the count at the critical values, and Section~\ref{sec:surface} introduces the function $R$ and proves Theorems~\ref{thm:count} and~\ref{thm:N}. Section~\ref{sec:examples} describes the certified examples, Section~\ref{sec:family} treats the family $(1,1,1,m_4)$, and Section~\ref{sec:degenerate} relates degeneracy to the mass map. In Section~\ref{sec:checks} we compare the results with the literature and describe the surface of critical values near its vertex. \emph{Notation.} Some letters have more than one meaning, which the indices and the context separate. The squared length of the outer side opposite body~$i$ is $R_i$, and the radius function of Theorem~\ref{thm:count} is $R$, with two arguments. In Section~\ref{sec:topology}, $R$ is a positive function on $S^1$; $R_c$ and $R_A$ are the radius functions of the curves $C_c$ and $C_A$ (Sections~\ref{sec:foldcurves}--\ref{sec:surface}), and $R_{\mathrm d}$ is that of the deltoid (Section~\ref{sec:checks}). The centre of mass is $c_m$, the counts are $c_i(m)$, a level of $A$ is $c$ (Sections~\ref{sec:idea}, \ref{sec:quantities} and~\ref{sec:thm1}--\ref{sec:examples}), and $c(s)$, with $c^*=c(s^*)$, is a coefficient of the $2$-jet of $G$ (Lemma~\ref{lem:jet}). In charts~$3$ and~$4$, $\sigma=1-s$ (Sections~\ref{sec:cert}--\ref{sec:critical}); $\sigma_m$ is the reflection in a mirror (Section~\ref{sec:critical}), and in Section~\ref{sec:family} $\sigma$ is the transposition of the bodies $2$ and~$3$. The angle from a mirror is $\tau=\varphi-\varphi_m$ (Sections~\ref{sec:band}, \ref{sec:critical} and~\ref{sec:proofN}), and $\tau_1$, $\tau_2$ are tangent vectors in Section~\ref{sec:restricted}. The bracket of the band lemma is bounded by $\beta$, and that of a band certificate by $\beta_C$ (Sections~\ref{sec:band}, \ref{sec:types} and~\ref{sec:cusppoints}), while $\beta_l$ are barycentric coordinates (Lemma~\ref{lem:convex}, Section~\ref{sec:restricted} and Data and code availability). Other uses of these letters, such as $\tau$ in Appendix~\ref{app:charts} and $\beta_1$, $\beta_2$ in the proof of Lemma~\ref{lem:fampitch}, are local to one proof or paragraph. \section{The Dziobek reduction and the mass map}\label{sec:setup} \subsection{Normalization} Since $\sum_im_i(x_j-x_i)=M(x_j-c_m)$, equation \eqref{eq:cc} is equivalent to \begin{equation}\label{eq:ccnorm} \sum_{i\ne j}m_i\,(x_i-x_j)\,\bigl(r_{ij}^{-3}-\lambda'\bigr)=0,\qquad j=1,\dots,4,\qquad \lambda'=\lambda/M . \end{equation} Equation \eqref{eq:ccnorm} is \cite[(57)--(58)]{Moe14} with $\lambda=M\lambda'$.\footnote{We cite the freely available lecture notes \cite{Moe14}, on which the chapter \cite{Moe15} is based.} Scaling the configuration by $t>0$ multiplies $\lambda'$ by $t^{-3}$. We fix $\lambda'=1$ and write $S_{ij}=r_{ij}^{-3}-1$. We call bodies $1$, $2$, $3$ the \emph{outer} bodies, since body $4$ is inside their triangle. Throughout, $(i,j,k)$ denotes a cyclic permutation of $(1,2,3)$. Let \begin{itemize}[leftmargin=2em] \item $a_i=|x_i-x_4|$, the spoke lengths; \item $\theta_i$ the angle at $x_4$ between $x_j$ and $x_k$; \item $R_i=r_{jk}^2=a_j^2+a_k^2-2a_ja_k\cos\theta_i$; \item $S_i=\frac12a_ja_k\sin\theta_i$, the area of the triangle $x_4x_jx_k$; \item $S=S_1+S_2+S_3$; \item $w_i=a_i^{-3}-1=S_{i4}$, $q_i=R_i^{-3/2}=S_{jk}+1$ and $k_i=w_i(q_i-1)$. \end{itemize} \begin{lemma}[Dziobek reduction]\label{lem:dziobek} Let $x$ be a concave CC with body $4$ strictly inside the triangle of the others, normalized by $\lambda'=1$. Then $01$, $k_1=k_2=k_3=:K<0$, $\theta\in(0,\pi)^3$ and $\theta_1+\theta_2+\theta_3=2\pi$. If moreover $m_4=1$, then \begin{equation}\label{eq:masses} m_i=\frac{S_i\,w_jw_k}{(-K)\,S},\qquad i=1,2,3 . \end{equation} Conversely, let $a\in(0,1)^3$ and $\theta\in(0,\pi)^3$ with $\sum_i\theta_i=2\pi$ and $k_1=k_2=k_3=K<0$, and place spokes of lengths $a_i$ at $x_4$ with these angles. Then this configuration, with the masses \eqref{eq:masses} and $m_4=1$, is a CC with $\lambda'=1$ and body $4$ inside. \end{lemma} \begin{proof} The configuration is planar and not collinear, that is, a Dziobek configuration. The barycentric identity $Sx_4=\sum_{i\le3}S_ix_i$ shows that the vector $\Delta=(S_1,S_2,S_3,-S)$ satisfies $\sum_l\Delta_l=0$ and $\sum_l\Delta_lx_l=0$. By Dziobek's relations \cite{Dzi00}, \cite[Prop.~26]{Moe14}, there is a real $\kappa\ne0$ with $m_im_jS_{ij}=\kappa\Delta_i\Delta_j$ for all $i\ne j$. For the pairs $(i,4)$ this reads $m_im_4w_i=-\kappa S_iS$. For the pairs $(j,k)$ it reads $m_jm_k(q_i-1)=\kappa S_jS_k$. Multiplying the two gives \[ k_i=-\kappa^2\,\frac{S_1S_2S_3\,S}{m_1m_2m_3m_4}, \] which is the same for all $i$ and negative. Next, $\kappa<0$. Otherwise $w_i<0$ and $q_i>1$: all spokes would be longer than $1$ and all sides of the outer triangle shorter than $1$. This is impossible: an interior point $p$ of a triangle with vertices $u,v,z$ satisfies $|p-u|<\max(|v-u|,|z-u|)$, by convexity of $|\cdot-u|$. From $\kappa<0$ we get $w_i>0$ (that is, $a_i<1$) and $q_i<1$ (that is, $R_i>1$). The interior position of $x_4$ puts the angles in $(0,\pi)$. With $m_4=1$ we have $m_i=-\kappa S_iS/w_i$. Substituting this and $m_4=1$ into the formula for $K=k_i$ gives $\kappa=w_1w_2w_3/(K S^2)$ and then \eqref{eq:masses}. Conversely, if we define $m_i$ by \eqref{eq:masses}, $m_4=1$ and $\kappa=w_1w_2w_3/(KS^2)$, a direct computation using $k_i=K$ shows that $m_im_jS_{ij}=\kappa\Delta_i\Delta_j$ for all six pairs. Then, for each $j$, \[ \sum_{i\ne j}m_iS_{ij}(x_i-x_j)=\frac{\kappa\Delta_j}{m_j}\Bigl(\sum_i\Delta_ix_i-\Bigl(\sum_i\Delta_i\Bigr)x_j\Bigr)=0, \] which is \eqref{eq:ccnorm} with $\lambda'=1$. With $\theta\in(0,\pi)^3$ and $\sum_i\theta_i=2\pi$, body~$4$ lies inside the triangle of the others. \end{proof} \begin{lemma}\label{lem:angles} For $a\in(0,1)^3$, the system $k_1=k_2=k_3=K$, with principal angles $\theta_i\in[0,\pi]$ and $\sum_i\theta_i=2\pi$, has at most one solution $(\theta,K)$, for either sign of $K$. Where the solution exists and $\theta\in(0,\pi)^3$, it depends analytically on $a$. \end{lemma} \begin{proof} The equation $k_i=K$ gives $R_i(K)=(1+K/w_i)^{-2/3}$, which is defined because $K=k_i>-w_i$. Since $dR_i/dK<0$, the function $\theta_i(K)=\arccos\bigl((a_j^2+a_k^2-R_i(K))/(2a_ja_k)\bigr)$ decreases strictly in $K$ where it is defined. Hence $\sum_i\theta_i(K)=2\pi$ has at most one solution. At a solution with $\theta\in(0,\pi)^3$ the derivative $\frac{d}{dK}\sum_i\theta_i$ is negative. Analyticity there follows from the implicit function theorem. \end{proof} \subsection{The configuration space and the mass map} Lemma~\ref{lem:angles} shows that the set \[ \Om=\bigl\{a\in(0,1)^3:\ \text{the solution of Lemma~\ref{lem:angles} exists, with }\theta\in(0,\pi)^3\text{ and }K<0\bigr\} \] is open. We call its points \emph{physical}. By Lemma~\ref{lem:dziobek}, $a\mapsto$ (configuration) is a bijection from $\Om$ onto the set of concave CCs with body $4$ inside, modulo similarity including reflection: the normalization $\lambda'=1$ fixes the scale, and $a$ and $\theta$ determine the configuration up to an isometry. The \emph{mass map} is the analytic map $F:\Om\to\R^3$ given by \begin{equation}\label{eq:F} \begin{gathered} F(a)=\mu=\Bigl(\log\frac{m_1}{m_4},\log\frac{m_2}{m_4},\log\frac{m_3}{m_4}\Bigr),\\ \mu_i=\hat m_i-\log(-K),\qquad \hat m_i=\log S_i+\log w_j+\log w_k-\log S , \end{gathered} \end{equation} and we write $J=\det\partial\mu/\partial a$ for its Jacobian determinant. Since multiplying all masses by a constant does not change the CCs, $c_4(m)=\#F^{-1}(\mu^{(4)}(m))$. It suffices to study the map $F=F_4$: for $i\ne4$ the map $F_i$ is defined in the same way after exchanging the labels $i$ and $4$. \subsection{Coordinates and symmetry}\label{sec:coords} With $E_1=(1,-1,0)/\sqrt2$ and $E_2=(1,1,-2)/\sqrt6$ we write \[ a=s(1,1,1)+xE_1+yE_2,\qquad x=r\cos\varphi,\quad y=r\sin\varphi . \] Then $s$ is the mean spoke length, $r$ is the distance from the axis $\{a_1=a_2=a_3\}$, and $\det\partial a/\partial(s,x,y)=\sqrt3$. \begin{itemize}[leftmargin=2em] \item The \emph{wedge} $W=\{a_1\ge a_2\ge a_3\}$ is $\{x\ge0,\ 30^\circ\le\varphi\le90^\circ\}$, whose two faces, the \emph{mirrors}, are $\varphi=90^\circ$ (where $a_1=a_2$) and $\varphi=30^\circ$ (where $a_2=a_3$). \item The symmetric group $\Sym$ permutes the outer bodies; $F$ is $\Sym$-equivariant. \item On the target we use $A=\frac13\sum_i\mu_i$, $P=(\mu_1-\mu_2)/\sqrt2$, $Q=(\mu_1+\mu_2-2\mu_3)/\sqrt6$, $G=(P,Q)$ and $\Theta=\atantwo(Q,P)$, for which $\det\partial(A,P,Q)/\partial\mu=1/\sqrt3$. \item Since the functions $(x,y)$ of $a$ and $(P,Q)$ of $\mu$ are given by the same linear formulas, the group $\Sym$ acts on the angle $\varphi$ and on the angle $\Theta$ by the same dihedral group. \item The functions $A$, $K$ and $J$ are $\Sym$-invariant, $J$ because the determinants of a permutation on the domain and on the target cancel. \item On the mirror $\varphi=90^\circ$ we have $\mu_1=\mu_2$, $P=0$ and $\Theta\in\{90^\circ,270^\circ\}$. On the mirror $\varphi=30^\circ$ we have $\mu_2=\mu_3$, $Q=P/\sqrt3$ and $\Theta\in\{30^\circ,210^\circ\}$. \end{itemize} Any statement about $W$ extends to $\Om$ by $\Sym$-equivariance. \subsection{The axis and the umbilic}\label{sec:axis} \begin{lemma}\label{lem:axis} On the axis $a=s(1,1,1)$ the following hold. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $\theta_i=2\pi/3$, $R_i=3s^2$ and $K=w(q-1)$, where $w=s^{-3}-1$ and $q=(\sqrt3\,s)^{-3}$. \item The point is physical if and only if $1/\sqrt31/\sqrt3$. (c) By \eqref{eq:masses}, $m=w^2/(3(-K))=w/(3(1-q))$, which is the stated formula. With $t=s^{-3}\in(1,3^{3/2})$ and $c=3^{-3/2}$, the ratio is $3(1-ct)/(t-1)$, whose derivative in $t$ is $3(c-1)/(t-1)^2<0$. As $t$ decreases in $s$, the ratio increases strictly in $s$. The ratio tends to $0$ as $s\downarrow1/\sqrt3$ and to $\infty$ as $s\uparrow1$. Setting it equal to $1$ gives $s^{-3}(1+1/\sqrt3)=4$. Finally $A=\frac13\sum_i\log(m_i/m_4)=\log(m/m_4)$. (d) On the axis $\mu_1=\mu_2=\mu_3$ and $P=Q=0$. It is fixed by $\Sym$, which acts on the $(x,y)$-plane and on the $(P,Q)$-plane by the same irreducible two-dimensional representation. The gradient of the invariant function $A$ in $(x,y)$ is a fixed vector of this representation and vanishes. The matrix $\partial(P,Q)/\partial(x,y)$ commutes with the representation. Commuting with the rotation by $120^\circ$ makes it a rotation-dilation. Commuting also with a reflection makes it a multiple of the identity. The matrix $\partial(A,P,Q)/\partial(s,x,y)$ is then the diagonal matrix with entries $\partial_sA$, $\lax$, $\lax$. Since its determinant is $\det\partial(A,P,Q)/\partial\mu\cdot J\cdot\det\partial a/\partial(s,x,y)=J$, we get $J=\partial_sA\,\lax^2$. \end{proof} Both factors of $J$ on the axis have closed forms. \begin{proposition}[the axis in closed form]\label{prop:ax} For $1/\sqrt30$ on $(1/\sqrt3,s^*)$, $\lax<0$ on $(s^*,1)$ and $\lax'(s^*)=-3(6\sqrt3-2)\,s^*/(1-s^{*3})<0$. At $s^*$ the mass ratio of Lemma~\ref{lem:axis}(c) is $m_4/m=m^*=(81+64\sqrt3)/249$, and $K=1/9-44\sqrt3/81$. In particular $J<0$ at every physical point of the axis other than $p^*=s^*(1,1,1)$, where $J=0$. \end{proposition} \begin{proof} We linearize the system of Lemma~\ref{lem:angles} at $a=s(1,1,1)$, $\theta=(2\pi/3)(1,1,1)$. With $R=3s^2$, $w=s^{-3}-1$ and $q=(\sqrt3\,s)^{-3}$ as in Lemma~\ref{lem:axis}(a), the partial derivatives of $k_i=w_i(q_i-1)$ there are \[ \eta_1=\frac{\partial k_i}{\partial a_i}=-3s^{-4}(q-1),\qquad \eta_2=\frac{\partial k_i}{\partial a_j}=-\frac92\,s\,w\,R^{-5/2},\qquad \eta_3=\frac{\partial k_i}{\partial\theta_i}=-\frac{3\sqrt3}2\,s^2\,w\,R^{-5/2} \] for $j\ne i$, while $k_i$ does not depend on $\theta_j$ for $j\ne i$. For a variation $\varepsilon$ of $a$ with $\sum_i\varepsilon_i=E$, the equations $\delta k_i=\delta K$ and $\sum_i\delta\theta_i=0$ have the solution $\delta K=(\eta_1+2\eta_2)E/3$ and $\delta\theta_i=(\eta_1-\eta_2)(E/3-\varepsilon_i)/\eta_3$. On the axis the matrix $\partial\mu/\partial a$ is symmetric under $\Sym$: its diagonal entries are $\alpha=\partial\mu_i/\partial a_i$ and its off-diagonal entries are $\beta=\partial\mu_i/\partial a_j$. Then $\lax=\partial_xP=\alpha-\beta$. Differentiating \eqref{eq:F} with the values above gives \[ \lax=\frac{\eta_1-\eta_2}{\sqrt3\,\eta_3}-\frac1s-\frac{w'}{w},\qquad w'=-3s^{-4}, \] which simplifies to the stated form. The formula for $\partial_sA$ follows from $A=\log(m/m_4)$ and the mass ratio of Lemma~\ref{lem:axis}(c); its sign follows from $s-1<0<9s^3-\sqrt3$ on $(1/\sqrt3,1)$. The numerator of $\lax$ decreases in $s$ and vanishes at $s^{*3}=3/(6\sqrt3-2)$, which lies between $(1/\sqrt3)^3$ and $1$. With $s(1-s^3)>0$ this proves the statements on the zero, the signs and $\lax'(s^*)$. Substituting $s^{*3}$ into the mass ratio $3(1-(\sqrt3\,s)^{-3})/(s^{-3}-1)$ and into $K=w(q-1)$ and rationalizing gives $m^*$ and $K(p^*)$. The last assertion follows from $J=\partial_sA\,\lax^2$ (Lemma~\ref{lem:axis}(d)). The script \texttt{axis\_lambda.py} repeats the linearization symbolically and checks these identities and evaluations in exact arithmetic. \end{proof} We call $\Sigma=\{J=0\}\subset\Om$ the \emph{fold} and $p^*=s^*(1,1,1)$ the \emph{umbilic}. By Lemma~\ref{lem:axis}(c),(d) and Proposition~\ref{prop:ax}, the fold meets the axis only at $p^*$, where $dF$ has rank one. This point is Palmore's degenerate configuration: the equilateral triangle with body $4$ at its centre and $m_4/m=m^*$ (Section~\ref{sec:checks}). It is also the point where $\Db$ splits into two pieces. A separate chart of the certificates covers a ball around it. We set $A^*=A(p^*)=-\log m^*$. In decimals $s^*=0.70970849110762766159\ldots$. The certificates use the two adjacent double-precision numbers \begin{gather*} [s_a,s_b]=[0.70970849110762757039\ldots,\ 0.70970849110762768141\ldots]. \end{gather*} Arb enclosures give $\lax(s_a)>0>\lax(s_b)$ (Proposition~\ref{prop:cert}(a)). These signs imply $s_a0$ such that \[ G(s,z)=\lambda(s)\,z+c(s)\,\bar z^{\,2}+E(s,z),\qquad |E(s,z)|\le C_E|z|^3\qquad(|s-s^*|\le\delta_s,\ |z|\le\delta_z). \] Here $\lambda=\lax$ and $\lambda(s^*)=0$. \end{lemma} \begin{proof} The map $G$ is real-analytic near $p^*$, an interior point of $\Om$, and $G(s,0)=0$ by Lemma~\ref{lem:axis}(d). Write $G(s,z)=\sum_{j+k\ge1}g_{jk}(s)z^j\bar z^k$. A cyclic permutation of the outer bodies acts on $z$ and on $G$ by the same rotation $z\mapsto\omega z$, $\omega=e^{\pm2\pi i/3}$. The resulting relation $g_{jk}\omega^{j-k}=\omega g_{jk}$ forces $g_{jk}=0$ unless $j-k\equiv1\pmod3$. Among the pairs with $j+k\le2$ this leaves $(1,0)$ and $(0,2)$. The transposition of the bodies $1$ and $2$ acts by $z\mapsto-\bar z$ on the domain and by $G\mapsto-\bar G$ on the target, which forces $g_{10}$ to be real and $g_{02}$ to be imaginary. We put $\lambda=g_{10}$ and $c=g_{02}$. Then $\lambda(s)=\partial_xP(s,0,0)=\lax(s)$. The bound on $E$ follows from Taylor's theorem in $(x,y)$, since the third derivatives are bounded on a compact neighbourhood. \end{proof} \begin{proposition}[the umbilic]\label{prop:U} In Lemma~\ref{lem:jet}, $c(s)=i\gamma(s)$ with \[ \gamma(s)=\frac{\sqrt2\,\bigl[(3888-22032\sqrt3)s^{12}+(22464-648\sqrt3)s^{9}-2841\sqrt3\,s^{6}+(486+8\sqrt3)s^{3}-11\sqrt3\bigr]}{12\,s^{2}(s-1)^{2}(s^{2}+s+1)^{2}(3\sqrt3\,s^{3}-1)^{2}} , \] and $\gamma(s^*)=-41.5719787\ldots<0$. In particular $c(s^*)\ne0$. Moreover $J(p^*)=0$, $\nabla J(p^*)=0$ and, in the coordinates $(s,x,y)$, \[ \operatorname{Hess}J(p^*)=\operatorname{diag}\bigl(2\,\partial_sA\,\lax'(s^*)^2,\ -8\,\partial_sA\,|c(s^*)|^2,\ -8\,\partial_sA\,|c(s^*)|^2\bigr), \] with $\partial_sA$ taken at $s^*$. This matrix has signature $(-,+,+)$. \end{proposition} \begin{proof} The coefficient $c(s)$ comes from the second-order expansion of the system of Lemma~\ref{lem:angles} about the axis, as in the proof of Proposition~\ref{prop:ax}. The script \texttt{axis\_jet2.py} carries out this expansion in exact arithmetic. It confirms that the coefficient of $\bar z$ of order one and the coefficients of $z^2$ and $z\bar z$ vanish, in agreement with Lemma~\ref{lem:jet}. It also produces $\lax$ and $c(s)$ in the stated forms. The evaluator of Section~\ref{sec:decide} gives an independent check. In ball arithmetic it computes the Taylor coefficients of $P$ and $Q$ at the axis point $s_b(1,1,1)$; its coefficient of $x^2$ in $Q$ agrees with the closed form of $\gamma(s^*)$ to $12$ digits. The denominator of $\gamma$ is positive at $s^*$, because $s^*\ne0,1$ and $3\sqrt3\,s^{*3}-1=(29+9\sqrt3)/52\ne0$. In the field $\mathbb Q(\sqrt3)$ the numerator, divided by $\sqrt2$, equals $-5827437/228488-(1875095/114244)\sqrt3<0$ at $s^{*3}=(3+9\sqrt3)/52$. The script \texttt{s3\_check.py} checks these two facts, and also $\lax'(s^*)<0$, in exact arithmetic. Thus $\gamma(s^*)<0$. For the Hessian we expand $J=\det\partial(A,P,Q)/\partial(s,x,y)$ (proof of Lemma~\ref{lem:axis}(d)) along its first row. The derivatives $\partial_xA$ and $\partial_yA$ vanish on the axis. So do $\partial_sP$ and $\partial_sQ$, because $P=Q=0$ on the axis. The derivatives of $P$ and $Q$ in $(x,y)$ vanish at $p^*$, where $\lax(s^*)=0$. Let $\varrho$ be the distance to $p^*$ in the coordinates $(s,x,y)$. The two cofactor terms are then $O(\varrho^3)$. Hence $J=\partial_sA\,(|G_z|^2-|G_{\bar z}|^2)+O(\varrho^3)$. Lemma~\ref{lem:jet} gives the $2$-jet $\lax'(s^*)(s-s^*)z+c(s^*)\bar z^2$ of $G$ at $p^*$, so $|G_z|^2-|G_{\bar z}|^2=\lax'(s^*)^2(s-s^*)^2-4|c(s^*)|^2|z|^2+O(\varrho^3)$. This implies $J(p^*)=0$, $\nabla J(p^*)=0$ and the stated Hessian, whose signature follows from $\partial_sA<0$, $\lax'(s^*)\ne0$ and $c(s^*)\ne0$. \end{proof} The proofs of Theorems~\ref{thm:count} and~\ref{thm:N} use only the inequality $c(s^*)\ne0$ of Proposition~\ref{prop:U}, in Proposition~\ref{prop:umbcount}, and the formalization proves it in Lean. Apart from the proof of this inequality, the closed form of $\gamma(s)$ and the Hessian of $J$ are used only in remarks, in Figure~\ref{fig:surface} and in Section~\ref{sec:checks}. By the Morse lemma, $\Db$ is a double cone near $p^*$ with its axis along the $s$-direction; in particular $\Db\cap\{s=s^*\}=\{p^*\}$ near $p^*$. The fold is asymptotic to the cone $r=|\lax'(s^*)|\,|s-s^*|/(2|c(s^*)|)$, of slope $0.3344\ldots$. The certificates will establish the global versions of these facts (Proposition~\ref{prop:cert}(e) and Section~\ref{sec:nappes}). \section{Formulas on the fold}\label{sec:fold} \subsection{The certified quantities}\label{sec:quantities} For a function $f$ of $(s,x,y)$ we write $\nabla f=(\partial_sf,\ \partial_rf,\ r^{-1}\partial_\varphi f)$ for its gradient in the frame $(e_s,e_r,e_\varphi)$, which is orthonormal and right-handed in the $(s,x,y)$-space. Let $\hA=\frac13\sum_i\hat m_i$. Then $A=\hA-\log(-K)$. The term $\log(-K)$ makes both $A$ and $J$ singular where $K=0$, while $P$ and $Q$ do not contain it. We multiply $\nabla A$ by $-K$ and define \begin{gather*} \Av=(-K)\nabla A=(-K)\nabla\hA+\nabla K,\qquad \Jt=\det[\Av;\nabla P;\nabla Q],\\ \hv=P\nabla Q-Q\nabla P=(P^2+Q^2)\nabla\Theta . \end{gather*} Note that these are analytic wherever $w_i>0$ and $S_i>0$, including across $K=0$. The certificates work with $\Jt$ in place of $J$, since $\Jt$ has the sign of $J$ on $\Om$ by Lemma~\ref{lem:foldformulas}(a). The vector $\hv$ is the gradient of the angle $\Theta$ of $G$, multiplied by $P^2+Q^2$ so that it stays analytic where $G=0$. On the fold $\Sigma$ we use \[ T_1=\partial_r\Jt,\qquad T_2=\Av_s(\nabla\Jt)_r-\Av_r(\nabla\Jt)_s,\qquad T_3=\det[\hv;\Av;\nabla\Jt], \] where the subscripts $s$, $r$ denote the components in the frame. At a point of $\Sigma$ with $T_1>0$ the ray crosses the fold transversally, from $J<0$ to $J>0$. Lemma~\ref{lem:foldformulas} shows that $T_2$ determines the sign of the derivative of $A|_\Sigma$ in $s$ and of $d\varphi$ along the curves $\Gamma=\Sigma\cap\{A=c\}$ and that $T_3$ determines the sign of $d\Theta$ along them. The signs $T_2<0$ and $T_3<0$ make $A|_\Sigma$ decrease in $s$ and $\Theta$ increase with $\varphi$ along $\Gamma$. \begin{lemma}\label{lem:foldformulas} \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $\Jt=(-K)\,J$. In particular $\operatorname{sign}\Jt=\operatorname{sign}J$ on $\Om$ and $\Sigma=\{\Jt=0\}\cap\Om$. \item At a point of $\Sigma$ with $T_1\ne0$, the fold is locally a graph $r=r_f(s,\varphi)$, on which the restriction $A|_\Sigma$ satisfies $\partial_s(A|_\Sigma)=T_2/((-K)\,T_1)$. \item The vector $v=\nabla A\times\nabla\Jt$ is tangent to the curve $\Gamma=\Sigma\cap\{A=c\}$, and \[ d\varphi(v)=\frac{T_2}{(-K)\,r},\qquad d\Theta(v)=\frac{T_3}{(P^2+Q^2)(-K)},\qquad \frac{d\Theta}{d\varphi}\Big|_\Gamma=\frac{r\,T_3}{(P^2+Q^2)\,T_2}. \] \end{enumerate} \end{lemma} \begin{proof} All three parts are direct computations. (a) As $\Av=(-K)\nabla A$ and the frame is orthonormal and right-handed, $\Jt=(-K)\det\partial(A,P,Q)/\partial(s,x,y)=(-K)\cdot\frac1{\sqrt3}\cdot J\cdot\sqrt3$. (b) By the implicit function theorem there is such an $r_f$; moreover $\partial_sr_f=-\partial_s\Jt/\partial_r\Jt$. Then $\partial_s(A|_\Sigma)=\partial_sA+\partial_rA\,\partial_sr_f=(\partial_sA\,\partial_r\Jt-\partial_rA\,\partial_s\Jt)/\partial_r\Jt$, whose numerator is $T_2/(-K)$. (c) The vector $v$, orthogonal to $\nabla A$ and $\nabla\Jt$, is tangent to both level sets. With $d\varphi(e_\varphi)=1/r$, its $e_\varphi$-component $(\nabla A)_s(\nabla\Jt)_r-(\nabla A)_r(\nabla\Jt)_s=T_2/(-K)$ gives the formula for $d\varphi(v)$. Also $d\Theta(v)=\det[\nabla\Theta;\nabla A;\nabla\Jt]=T_3/((P^2+Q^2)(-K))$. The last formula is the quotient of the first two. \end{proof} \subsection{The mirror identity}\label{sec:mirror} For a mirror angle $\varphi_m\in\{30^\circ,90^\circ\}$ we put \[ L=\cos\varphi_m\,P+\sin\varphi_m\,Q,\qquad L^\perp=-\sin\varphi_m\,P+\cos\varphi_m\,Q,\qquad \Jm=\Av_s\,\partial_rL-\Av_r\,\partial_sL , \] and for $\varphi_m=90^\circ$ we have $L=Q$ and $L^\perp=-P$. \begin{lemma}[mirror identity]\label{lem:mirror} On the mirror $\varphi=\varphi_m$, \[ \Jt=\frac{\partial_\varphi L^\perp}{r}\,\Jm,\qquad T_3=L\,\frac{\partial_\varphi L^\perp}{r}\,T_2 . \] Wherever $\Jm\ne0$ on the mirror, $T_3=(L\,T_2/\Jm)\,\Jt$. In particular $T_3=0$ at every point of $\Sigma$ on the mirror at which $\Jm\ne0$. \end{lemma} \begin{proof} As the pair $(L,L^\perp)$ is obtained from $(P,Q)$ by a rotation, $\Jt=\det[\Av;\nabla L;\nabla L^\perp]$ and $\hv=L\nabla L^\perp-L^\perp\nabla L$. The reflection in the mirror, which exchanges two outer bodies, fixes $A$, $K$, $\Jt$ and $L$ and changes the sign of $L^\perp$. On the mirror it follows that $L^\perp=\partial_sL^\perp=\partial_rL^\perp=0$ and $\partial_\varphi A=\partial_\varphi K=\partial_\varphi L=\partial_\varphi\Jt=0$. Then $\nabla L^\perp=(0,0,r^{-1}\partial_\varphi L^\perp)$ and $\hv=(0,0,L\,r^{-1}\partial_\varphi L^\perp)$, while $\Av$, $\nabla L$ and $\nabla\Jt$ have vanishing third components. Expanding the two determinants along the third column, respectively the first row, gives the two formulas. \end{proof} \subsection{The band lemma}\label{sec:band} Lemma~\ref{lem:mirror} shows that $T_3=0$ at the points of $\Sigma$ on a mirror at which $\Jm\ne0$. An enclosure of $T_3$ over a box that contains such a point cannot certify $T_3<0$. The band lemma replaces this test near the mirrors. The reflection in a mirror $\varphi_m$ reverses orientation and changes $\Theta$ into $\mathrm{const}-\Theta$, while it fixes $A$, $K$, $\Jt$ and $P^2+Q^2$. These two sign changes cancel in $T_3=(P^2+Q^2)(-K)\det[\nabla\Theta;\nabla A;\nabla\Jt]$, making $T_3$ and $\Jt$ even in $\tau=\varphi-\varphi_m$ at fixed $(s,r)$. \begin{lemma}[band lemma]\label{lem:band} Let $C$ be a box in the coordinates $(s,r,\varphi)$ whose $\varphi$-range contains $\varphi_m$ and on which $\Jt$ and $T_3$ are analytic, and let $C_m=C\cap\{\varphi=\varphi_m\}$. Suppose that $\Jm\ne0$ and $T_1\ne0$ on $C_m$, that for every $s$ in the $s$-range of $C$ the function $\Jt(s,\cdot,\varphi_m)$ has a zero in the $r$-range of $C$, and that \[ \partial_\varphi^2T_3(\xi_1)-\frac{\partial_rT_3(\xi)}{T_1(\xi')}\,\partial_\varphi^2\Jt(\xi_2)\le\beta\qquad\text{for all }\xi_1,\xi_2\in C\text{ and }\xi,\xi'\in C_m \] for some $\beta<0$. Then every zero $(s,r,\varphi_m+\tau)$ of $\Jt$ in $C$ satisfies \begin{equation}\label{eq:bandquant} T_3(s,r,\varphi_m+\tau)\le\tfrac{\tau^2}{2}\,\beta . \end{equation} In particular $T_3<0$ at every point of $C$ off the mirror at which $\Jt=0$. \end{lemma} \begin{proof} Let $(s,r,\varphi_m+\tau)\in C$ with $\Jt=0$ there. For $\tau=0$ the claim is $T_3\le0$, which holds by Lemma~\ref{lem:mirror} because $\Jm\ne0$ on $C_m$. We assume $\tau\ne0$. By evenness and Taylor's theorem in $\tau$ at fixed $(s,r)$, \[ T_3(s,r,\varphi_m+\tau)=T_3(s,r,\varphi_m)+\tfrac{\tau^2}{2}\,\partial_\varphi^2T_3(\xi_1),\qquad 0=\Jt(s,r,\varphi_m)+\tfrac{\tau^2}{2}\,\partial_\varphi^2\Jt(\xi_2), \] for some $\xi_1,\xi_2\in C$. Let $(s,r_m,\varphi_m)\in C_m$ be a zero of $\Jt$, which exists by hypothesis and at which $T_3=0$ by Lemma~\ref{lem:mirror}. The mean value theorem in $r$ on $C_m$ shows that $T_3(s,r,\varphi_m)=\partial_rT_3(\xi)\,(r-r_m)$ and $\Jt(s,r,\varphi_m)=T_1(\xi')\,(r-r_m)$ with $\xi,\xi'\in C_m$. Dividing, we get $T_3(s,r,\varphi_m)=\bigl(\partial_rT_3(\xi)/T_1(\xi')\bigr)\,\Jt(s,r,\varphi_m)$. Combining, \[ T_3(s,r,\varphi_m+\tau)=\frac{\tau^2}{2}\Bigl(\partial_\varphi^2T_3(\xi_1)-\frac{\partial_rT_3(\xi)}{T_1(\xi')}\,\partial_\varphi^2\Jt(\xi_2)\Bigr)\le\frac{\tau^2}{2}\,\beta .\qedhere \] \end{proof} We verify the hypothesis on the bracket from enclosures of the four quantities over $C$ and $C_m$. In exact rational arithmetic we evaluate the bracket at the corners of the enclosures and take for $\beta$ the largest corner value, which must be negative. This is valid: for $d$ of one sign, $tj/d$ is monotone in each of $t$, $j$ and $d$ separately. So the extreme values of $tj/d$ over a product of intervals are attained at corners. In the top chart~3 of Section~\ref{sec:charts} the lemma is used with $\hat r$ in place of $r$. On the ball around the umbilic (chart~2) it is applied at fixed $\varrho$ with $\psi$ in place of $r$. There the quantities $\Jt/\varrho^2$ and $T_3/\varrho^4$ replace $\Jt$ and $T_3$. For $\varrho>0$ they have the signs of $\Jt$ and $T_3$. The derivative $\partial_\psi(\Jt/\varrho^2)$ replaces $T_1$ and is only required to be nonzero on the mirror face. The derivative $\partial_\psi(T_3/\varrho^4)$ replaces $\partial_rT_3$. A zero of $\Jt/\varrho^2$ is required on each $\psi$-segment of the mirror face. \section{Lemmas on the physical region}\label{sec:hand} This section collects facts about the physical points. Lemmas~\ref{lem:B1}--\ref{lem:alpha} bound the region that the covers of Section~\ref{sec:cert} must cover; the covers are set up on these bounds. Lemmas~\ref{lem:K0} and~\ref{lem:convex} control the face $K=0$ of $\Om$. The proofs are elementary and by hand. The proof of Lemma~\ref{lem:convex}(b) takes a derivative on this face from Lemma~\ref{lem:face}(b); the proof of Lemma~\ref{lem:face} in Section~\ref{sec:restricted} rests only on Lemmas~\ref{lem:dziobek} and~\ref{lem:angles}. \begin{lemma}[a priori bounds]\label{lem:B1} Every physical $a$ satisfies $r\le\sqrt6\max_i(a_i-s)$, $r<\sqrt6\,(2s-1)$ and $r<\sqrt6\,(1-s)$. In particular $s>\frac12$. \end{lemma} \begin{proof} A unit vector of the plane $\sum_id_i=0$ has largest coordinate at least $1/\sqrt6$. Applied to $(a-s(1,1,1))/r$, this proves the first inequality. Since $R_i>1$ and $\theta_i<\pi$, we have $a_j+a_k>r_{jk}>1$. Then $a_i=3s-a_j-a_k<3s-1$ and $\max_i(a_i-s)<2s-1$. Finally $a_i<1$ implies $\max_i(a_i-s)<1-s$. \end{proof} \begin{lemma}[Fermat-point bound]\label{lem:fermat} Every physical point has $s>1/\sqrt3$. \end{lemma} \begin{proof} Let $L_F$ be the least value of the sum of the distances from a point to the vertices of the outer triangle, whose sides $b_1,b_2,b_3$ all exceed $1$. Then $3s=\sum_ia_i\ge L_F$. If all angles of the triangle are less than $120^\circ$, then $L_F^2=\frac12(b_1^2+b_2^2+b_3^2)+2\sqrt3\,\mathrm{Area}$. With $\beta_1$ the angle opposite $b_1$ we then have $\partial L_F^2/\partial b_1=2b_1\sin(\beta_1+60^\circ)/\sin\beta_1>0$ at fixed $b_2,b_3$. Shrinking the largest side to the second largest and then both to the smallest keeps all angles below $120^\circ$ and decreases $L_F$. Thus $L_F\ge\sqrt3\min_lb_l>\sqrt3$. If some angle is at least $120^\circ$, then $L_F$ is the sum of the two shorter sides and exceeds $2$. \end{proof} \begin{lemma}[$\alpha$-test]\label{lem:alpha} If $a_j+a_k\le1$ for some pair, then $a$ is not physical. Otherwise the numbers $\zeta_i=(a_j^2+a_k^2-1)/(2a_ja_k)$ exceed $-1$. With $\alpha_i=\arccos(\min(\zeta_i,1))$, if $\sum_i\alpha_i\ge2\pi$, then $a$ is not physical. \end{lemma} \begin{proof} A physical point has $a_j+a_k>1$ by the proof of Lemma~\ref{lem:B1}. It also has $R_i>1$, which is equivalent to $\cos\theta_i<\zeta_i$ and implies $\theta_i>\alpha_i$ for all $i$. Summing, $2\pi=\sum_i\theta_i>\sum_i\alpha_i$. \end{proof} \begin{lemma}[$K=0$ lemma]\label{lem:K0} Let $a\in(0,1)^3$ be a point at which the solution of Lemma~\ref{lem:angles} exists, with $\theta\in(0,\pi)^3$ and $K=0$. Then $1/\sqrt3\le s<2/3$, and in particular $s8/27$ by Proposition~\ref{prop:ax}, that is, $s^*>2/3$. \end{proof} \begin{lemma}[angle-sum lemma]\label{lem:convex} Let $g_\alpha=\sum_i\alpha_i$, with $\zeta_i$ and $\alpha_i$ as in Lemma~\ref{lem:alpha}. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item Let $a\in(0,1)^3$, with $a_j+a_k>1$ for every pair, be a point at which the solution of Lemma~\ref{lem:angles} exists with $\theta\in(0,\pi)^3$. Then $K<0$ if and only if $g_\alpha(a)<2\pi$. \item Let $a=a(s,r,\varphi)$ with $r>0$ satisfy the hypotheses of Lemma~\ref{lem:K0}. Then there is $\epsilon>0$ such that no point $a(s,t,\varphi)$ with $r1$ and $\theta_i>\alpha_i$ for all $i$. Summing these inequalities, we obtain $g_\alpha<\sum_i\theta_i=2\pi$. For $K\ge0$ we have $R_i\le1$, $\zeta_i\le\cos\theta_i\le1$ and $\theta_i\le\alpha_i$ for all $i$, which implies $g_\alpha\ge2\pi$. (b) The point $a$ lies on the face $\mathcal K$ of Section~\ref{sec:restricted}, where $K=0$. By Lemma~\ref{lem:face}(a) its configuration is $(v_1,v_2,v_3,p)$ up to an isometry, for a point $p$ inside the unit equilateral triangle $v_1v_2v_3$ of that section, and $\theta_i=\alpha_i=\arccos\zeta_i$. Hence $|\zeta_i|<1$, so that $g_\alpha$ is analytic near $a$. Moreover $a_j+a_k>|v_j-v_k|=1$ for every pair, and (a) gives $g_\alpha(a)\ge2\pi$. The barycentric coordinates $\beta_l=\frac13+2\,p\cdot v_l$ of $p$ are positive, and Lemma~\ref{lem:face}(b) gives $\partial g_\alpha/\partial a_l=-(2/\sqrt3)\,a_l\beta_l/(\beta_1\beta_2\beta_3)$ at $a$. As $|v_l|^2=\frac13$ and $\sum_lv_l=0$, we have $a_l^2=|p|^2+\frac13-2\,p\cdot v_l$ and $\sum_la_l^2=3|p|^2+1$, hence $\beta_l=\frac13\bigl(\sum_ia_i^2+1\bigr)-a_l^2$. Put $e=a-s(1,1,1)$, so that $\partial_ra=e/r$, $\sum_le_l=0$ and $\sum_le_l^2=r^2$. Since $\sum_le_l=0$, also $\sum_le_l^4=r^4/2$ and $r^6-6\bigl(\sum_le_l^3\bigr)^2=2\prod_{j1$. The function $t\mapsto2s^2-\frac13+\frac{t^2}6-\frac{3st}{\sqrt6}$ decreases on $[0,\sqrt6\,(2s-1)]$, since its minimum lies at $t=9s/\sqrt6>\sqrt6\,(2s-1)$, and it equals $\frac23-s$ at $t=\sqrt6\,(2s-1)$. Therefore $\sum_la_l\beta_le_l<-r^2\bigl(\frac23-s\bigr)<0$, and \[ \partial_rg_\alpha(a)=\sum_l\frac{\partial g_\alpha}{\partial a_l}\,\frac{e_l}r=-\frac2{\sqrt3}\,\frac{\sum_la_l\beta_le_l}{r\,\beta_1\beta_2\beta_3}>0 . \] So $g_\alpha>2\pi$ at the points $a(s,t,\varphi)$ with $t>r$ close to $r$, and Lemma~\ref{lem:alpha} shows that these points are not physical. \end{proof} \section{The certificates}\label{sec:cert} The certificates are finite covers of parts of the configuration space by closed boxes, the \emph{leaves}. Each leaf carries enclosures of the quantities required for its certificate, computed in ball arithmetic. It also carries a \emph{type}, which states the property certified on it by these enclosures. In this section we describe the enclosures, the charts, the covers, the types, the inclusion argument and the checks that we run on them. Most leaves, $1\,426\,826$ of $1\,852\,313$, belong to the bulk cover (Section~\ref{sec:covers}), which certifies only that $J>0$ or that there is no physical point. The delicate certificates are those of the umbilic chart (Section~\ref{sec:balls}) and the band certificates (Section~\ref{sec:types}), where the quantities to be signed vanish. Proposition~\ref{prop:cert} at the end lists the computational results used in the proof of Theorem~\ref{thm:count}, together with item (g), which identifies the concave CCs of four equal masses (Section~\ref{sec:results}). \subsection{Ball arithmetic and the principal branch}\label{sec:balls} We compute all enclosures of the certified quantities with the library Arb \cite{Joh17}, which is now part of FLINT \cite{FLI25}. For interval methods and their use in proofs see \cite{Moo66,Neu90,MKC09,Tuc11}. Arb computes with balls, intervals $[c-\varepsilon,c+\varepsilon]$ with floating-point centre $c$ and radius $\varepsilon$; its operations return balls that contain the exact results for all points of the input balls. The tests below rely on the following properties of Arb, which we test on example balls (Section~\ref{sec:checklist}). The logarithm and the power with exponent $-3/2$ of a ball that meets $(-\infty,0]$ are balls with a NaN midpoint. So is the reciprocal of a ball that contains $0$. A NaN midpoint survives addition, multiplication, also by an exact zero, and intersection with a finite ball. Arb does not report a ball with a NaN midpoint as contained in a finite ball. A ball of infinite radius about a finite midpoint, however, becomes finite when it is intersected with a finite ball. This is sound, since the intersection of two enclosures is an enclosure. The principal-branch argument below uses the property of the logarithm. The code relies on the other properties to make an evaluation fail when an intermediate value has a NaN midpoint, also at the centre of a Taylor form. \emph{The fold-core charts.} For a box in one of the charts $0$--$4$ of Section~\ref{sec:charts}, we compute enclosures over a ball $c\pm h$ in chart coordinates that contains the box. We use Taylor forms of order $p$: the jet of each quantity at the centre up to degree $p-1$, together with the coefficients of degree $p$ of the jet computed with the whole ball as base point. The implicit angles are the solution $(\theta_1,\theta_2)$ of $C(a,\theta)=(k_1-k_2,\,k_1-k_3)=0$ with $\theta_3=2\pi-\theta_1-\theta_2$. We set $K=(k_1+k_2+k_3)/3$. We enclose the angles by a Krawczyk step \cite{Kra69}. It rests on the following criterion (see \cite{Moo77}, \cite[Ch.~5]{Neu90} and \cite[Ch.~8]{MKC09}). Let $V$ be a box with centre $\hat v$ and $Y$ an invertible matrix. If the interval evaluation of $\hat v-YC(a,\hat v)+(I-Y\,C_\theta(a,V))(V-\hat v)$ over all $a$ of the ball lies in the interior of $V$, then for each $a$ of the ball the equation $C(a,\cdot)=0$ has exactly one solution in $V$. A box is \emph{resolved} if this step succeeds over the whole ball. Each resolved evaluation also has a finite enclosure of $\hA$, which forces the principal branch. Indeed, $\hA$ is computed from the Arb logarithms of $w_i$, $S_i$ and $S$. A finite enclosure of $\hA$ implies $w_i>0$ (that is, $00$ on the ball, hence $\sin\theta_i>0$ for $i=1,2,3$. As all quantities depend on $\theta$ only through $\cos\theta_i$ and $\sin\theta_i$, the representatives of the $\theta_i$ modulo $2\pi$ in $(0,\pi)$ solve the same equations. Their sum is a multiple of $2\pi$ in $(0,3\pi)$, that is, $2\pi$. By the uniqueness in Lemma~\ref{lem:angles}, the enclosed solution is the solution of that lemma and has $\theta\in(0,\pi)^3$. On a resolved box, $K$, $\hA$, $P$, $Q$, $\Jt$ and the other quantities of Section~\ref{sec:fold} are therefore the analytic functions defined there. A point of the box is physical exactly when $K<0$ there. \emph{The umbilic chart.} Since the quantities $\Jt$, $T_1$, $T_2$ and $T_3$ all vanish at $p^*$, their enclosures over boxes that contain $p^*$ cannot have strict signs. In a separate chart we divide them by powers of the distance $\varrho$ to $p^*$ in the $(s,x,y)$-space. All first derivatives of $P$ and $Q$ vanish at $p^*$. The derivatives in $s$ vanish on the axis, where $P=Q=0$. The derivatives in $(x,y)$ form the matrix $\lax(s^*)\,I$ at $p^*$ (Lemma~\ref{lem:axis}(d)), which is $0$. Near $p^*$, then, $P,Q=O(\varrho^2)$, $\nabla P,\nabla Q=O(\varrho)$, $\Jt=O(\varrho^2)$, $\hv=O(\varrho^3)$, $T_1,T_2,\Jm=O(\varrho)$ and $T_3=O(\varrho^4)$. In chart~$2$ we certify the quantities divided by the matching power of $\varrho$, among them $\Jt/\varrho^2$, $P/\varrho^2$, $Q/\varrho^2$, $T_1/\varrho$, $T_2/\varrho$, $T_3/\varrho^4$, $\Jm/\varrho$ and $\partial_\psi(\Jt/\varrho^2)$, each of which has the sign of the undivided quantity for $\varrho>0$. We expand at $p^*$ the base quantities $K$, $\Jt$, $T_3$, $P$, $Q$ with their partial derivatives up to the orders required by the certificates, together with the vector $\Av=(-K)\nabla A$. For a base quantity $f$ of order $\nu$ whose jet is valid to degree $n$, \[ f(p^*+\varrho w)/\varrho^\nu=\sum_{\nu\le|\alpha|\pi$ and $K=K^*$ we have $0K_{\pi,2},K_{\pi,3}$ and that \[ \bar q=\max_{[\pi,\theta_1^{\max}]}k_1'\cdot\max\Bigl(\frac1{|k_2'|}+\frac1{|k_3'|}\Bigr)<1, \] where the second maximum is taken over the ranges of $\theta_2$ and $\theta_3$ on the box, enlarged on both sides by $\delta_2\ge0$ and $\delta_3\ge0$, respectively. The check also certifies $\delta_i\ge\max_{[\pi,\theta_1^{\max}]}k_1'\cdot\max(1/|k_i'|)\cdot(\theta_1^{\max}-\pi)$ for $i=2,3$, the second maximum over the enlarged ranges, so that the enlarged ranges contain all values of $\theta_2$ and $\theta_3$ during the decrease. Consequently $\theta_2+\theta_3$ grows by at most $\bar q(\theta_1^*-\pi)$, which gives $\sum_i\theta_i(K_{\pi,1})\le2\pi-(1-\bar q)(\theta_1^*-\pi)<2\pi$. Since the angles $\theta_i(K)$ are all less than $\pi$ only if $K>K_{\pi,1}$, the monotonicity in Lemma~\ref{lem:angles} leaves no solution with $\theta\in(0,\pi)^3$. \item By the continuation check, all physical points of a resolved box lie on the enclosed branch with $\theta_1<\pi$. There $k_i'<0$ and $\Lambda>0$. Moreover $\det\mathcal N'=\sin\theta_1\,\Lambda^3J$, or $\sin\theta_1\,(-K)\,\Lambda^3J$ with the rows used near $K=0$. \item A leaf of type P is resolved and has $\det\mathcal N'>0$ and $\Lambda>0$ on the box. By the previous item, $J>0$ at its physical points. \item Five tests show that a box holds no physical point. A leaf whose box passes one of them has type X. \begin{enumerate}[label=\textup{(\roman*)},leftmargin=2em] \item The branch test: the enclosed branch has $\theta_1>\pi$ throughout the box and passes the continuation check. \item The test at $K_{\pi,1}$: throughout the box, $K_{\pi,1}>K_{\pi,2},K_{\pi,3}$ and $\theta_2+\theta_3<\pi$ at $K=K_{\pi,1}$, hence $\sum_i\theta_i(K)<2\pi$ whenever all $\theta_i(K)<\pi$. \item The range test: throughout the box, some $a_i\ge1$ or some $a_j+a_k\le1$. \item The test at $K=0$: throughout the box, $\sum_i\theta_i(0)\ge2\pi$, hence $\sum_i\theta_i(K)>2\pi$ for $K<0$. \item The sign test: the enclosed branch has $K\ge0$ throughout the box and passes the continuation check where it reaches $\theta_1\ge\pi$. \end{enumerate} \end{itemize} \subsection{The charts}\label{sec:charts} Table~\ref{tab:charts} lists the charts, in each of which all the quantities are analytic up to the faces of the chart domain that are used. In charts $3$ and $4$ the $w_i$, the $k_i$ and $K$ all carry a factor $\sigma$. We divide it out. The scaled equations stay regular at $\sigma=0$. There the scaled value $\widetilde K=K/\sigma$ is negative. In these charts the proof uses $\widetilde K$ only in the test $\widetilde K<0$ for physical points and in the function $A-\log\sigma=\hA-2\log\sigma-\log(-\widetilde K)$, which the programs compute from the scaled weights $w_i/\sigma$ and from whose gradient they obtain $\nabla A$. The frame of Section~\ref{sec:quantities} is replaced by $(-\sigma\partial_\sigma,\partial_{\hat r},\hat r^{-1}\partial_\varphi)$ in chart~$3$ and by $(-\sigma\partial_\sigma,\partial_\xi,\partial_\eta)$ in chart~$4$. In chart~$3$ this frame is $\sigma M'$ times the frame of chart~$1$, where $M'$ is a shear with $\det M'=1$. Chart~$4$ is related to chart~$0$ in the same way. With $\Av$ replaced by $\nabla A$, the formulas of Section~\ref{sec:quantities} give $\Jt=\sigma^3\Jt_1/(-K)$, where $\Jt_1$ is the value in chart~$1$ and $K=\sigma\widetilde K<0$ is the unscaled value. In particular $\operatorname{sign}\Jt=\operatorname{sign}J$. At the points of $\Sigma$, $T_1$, $T_2$ and $T_3$ are the values in chart~$1$ multiplied by positive factors. In particular $T_3=\sigma^6T_3^{(1)}/K^2$ at the zeros of $\Jt$, where $T_3^{(1)}$ is the value in chart~$1$, because the three rows of the determinant are $\sigma M'\hv$, $\sigma M'\Av/(-K)$ and $\sigma M'\nabla(\sigma^3\Jt_1/(-K))=\sigma^4M'\nabla\Jt_1/(-K)$ there. At every point $\Jm=\sigma^2\Jm^{(1)}/(-K)$, where $\Jm^{(1)}$ is the value in chart~$1$: the shear cancels in the $2\times2$ determinant. \begin{table}[ht] \centering\small \begin{tabular}{@{}ll>{\raggedright\arraybackslash}p{1.6in}@{}} \toprule chart & coordinates & region\\ \midrule $0$ & $(s,x,y)$ & near the axis\\ $1$ & $(s,\ l=\log_2r,\ \varphi)$ & the fold core away from the axis\\ $2$ & $(\varrho,\psi,\varphi)$, $(s,x,y)=p^*+\varrho(\cos\psi,\sin\psi\cos\varphi,\sin\psi\sin\varphi)$ & the ball around the umbilic\\ $3$ & $(\sigma,\hat r,\varphi)$, $s=1-\sigma$, $r=\sigma\hat r$ & the fold core near $a=(1,1,1)$\\ $4$ & $(\sigma,\xi,\eta)$, $s=1-\sigma$, $x=\sigma\xi$, $y=\sigma\eta$ & the axis near $a=(1,1,1)$\\ $\mathrm{CH}_{110}$ & $u=\bigl(a_3,\ (1-a_2)/a_3,\ (1-a_1)/(1-a_2)\bigr)$ & the corner $a\to(1,1,0)$\\ $\mathrm{CH_{fin}}$ & $u=(-K,\ a_3,\ \theta_1)$ & the fin $a_1+a_2\to2$\\ $\mathrm{CH}_{111}$ & $u=\bigl(1-a_3,\ (1-a_2)/(1-a_3),\ (1-a_1)/(1-a_2)\bigr)$ & the corner $a\to(1,1,1)$ and the fin tip\\ bulk & $(s,x,y)$ & the rest of the wedge\\ \bottomrule \end{tabular} \par\vspace{6pt} \caption{The charts of the certificates. The fold core is defined in Section~\ref{sec:covers}.}\label{tab:charts} \end{table} \subsection{The covers}\label{sec:covers} We use the functions $\rtop$ and $\rax$ defined below and the constants \[ \sB=\tfrac{19}{32},\qquad \sH=\tfrac{31}{32},\qquad \rhtop=\tfrac3{16},\qquad \varrho_{\mathrm u}=7.5\cdot10^{-4}. \] More precisely, $\varrho_{\mathrm u}$ is the smallest double-precision number not below $7.5\cdot10^{-4}$, the double nearest to it, which the programs use. It exceeds $7.5\cdot10^{-4}$ by $1.6\cdot10^{-20}$. The \emph{fold core} is the following region. \begin{itemize}[leftmargin=2em] \item For $s\in(\frac12,\sB]$: $r\le\sqrt6\,(2s-1)$, which holds at all physical points by Lemma~\ref{lem:B1}. \item For $s\in[\sB,\sH]$: $r\le\rtop(s)$. \item For $s\ge\sH$: $\hat r\le\rhtop$, in the coordinates of chart~$3$. \end{itemize} At $s=\sB$ and $s=\sH$, where two descriptions apply, the fold core is their union. We write $FC(s)$ for the part of the fold core at level $s$. Table~\ref{tab:covers} lists the covers, and the leaves of the covers of charts~$0$ and~$1$ that meet the mirror planes are drawn in Figure~\ref{fig:fold}. The \emph{zone column} $\{s\in[0.70941162109375,\,0.7099609375],\ r\le\rtop(s)\}$ is a neighbourhood of the umbilic, which the umbilic cover covers. In the fold-core charts, $\varphi$ ranges over $[\pi/6-10^{-12},\,\pi/2+10^{-12}]$. \begin{table}[ht] \centering\small \begin{tabular}{@{}lp{0.55in}>{\raggedright\arraybackslash}p{2.35in}>{\raggedright\arraybackslash}p{1.95in}@{}} \toprule cover & chart & region & leaves\\ \midrule core & $1$ & $s\in[\sB,\sH]$, $\rax\le r\le\rtop$, off the zone column & M~$82252$, P~$231367$, F~$36031$, X~$2808$, B~$2334$, U~$67$\\ axis & $0$ & $s\in[\sB,\sH]$, $r\le\rax$, off the zone column & M~$4576$\\ lower core & $1$ & $s\in[\frac12,\sB]$, $\rax\le r\le\sqrt6(2s-1)$ & M~$12818$, P~$2111$, F~$1665$, X~$21661$, B~$25$\\ lower axis & $0$ & $s\in[\frac12,\sB]$, $r\le\rax$ & M~$109$, X~$293$\\ top core & $3$ & $\sigma\le2^{-5}$, $2^{-5}\le\hat r\le\rhtop$ & M~$3984$, P~$10607$, F~$1293$, B~$27$\\ top axis & $4$ & $\sigma\le2^{-5}$, $\hat r\le2^{-5}$ & M~$208$\\ umbilic & $2$ & $\varrho\le\varrho_{\mathrm u}$ around $p^*$ & M~$26$, P~$114$, F~$14$, B~$2$\\ bulk & bulk & $s\in[\sB,\sH]$: the part of the wedge outside the core, the fin and the corner & P~$443963$, X~$982831$, D~$32$\\ corner $(1,1,0)$ & $\mathrm{CH}_{110}$ & $u\in[0,0.1875]\times[0,1]^2$ & P~$792$, X~$744$\\ fin & $\mathrm{CH_{fin}}$ & $u\in[0,0.08]\times[0.125,0.9]\times[\pi/2,\pi]$ & P~$485$, X~$870$\\ corner $(1,1,1)$ & $\mathrm{CH}_{111}$ & $u\in[0,0.1]\times[0,1]^2$ & P~$1281$, X~$6757$, D~$166$\\ \bottomrule \end{tabular} \par\vspace{6pt} \caption{The covers and the numbers of their leaves of each type (Section~\ref{sec:types}). Of the leaves of type X, $1195$ in the core cover, $3113$ in the lower core cover and $14$ in the lower axis cover have $K>0$ on a resolved box. The other $1613$, $18548$ and $279$ are excluded by the $\alpha$-test.}\label{tab:covers} \end{table} \begin{figure}[tp] \centering \includegraphics[width=\textwidth]{fig_fold.pdf} \caption{The leaves of the core, lower core, axis and lower axis covers that meet the mirror planes $\varphi=90^\circ$ (top) and $\varphi=30^\circ$ (bottom), drawn in the $(s,r)$-plane with $r$ on a logarithmic scale and coloured by type (Table~\ref{tab:types}). The leaves of type U, which lie in the umbilic ball, are not drawn. The legend gives the certified signs of $\Jt=(-K)J$, which are those of $J$ at the physical points (Lemma~\ref{lem:foldformulas}(a)). Leaves of type B, which are thinner than a line at this scale, are drawn one line high. The leaves of type M reach the bottom edge of the plot, $r=2^{-16}$. They lie below the fold, except for $s$ below about $0.59$, where the rays in the mirror planes do not meet the fold (case (R2) of Corollary~\ref{cor:dichotomy}) and the leaves of type M lie directly below leaves of type X. Those of type X on the left contain no physical point: physical points have $s>1/\sqrt3$ (Lemma~\ref{lem:fermat}). The leaves of type X above the others, for $s<0.61$, contain no physical point either. They have $K>0$ or are excluded by the $\alpha$-test (Table~\ref{tab:covers}). For $s\ge19/32$ the region above the drawn leaves is that of the bulk cover, where $J>0$. For $s<19/32$ no physical point lies above $r=\sqrt6\,(2s-1)$ (Lemma~\ref{lem:B1}). Neither the zone column around $s^*$, covered by the umbilic cover and narrower than the dotted line at $s^*$, nor the strip $s\ge31/32$, covered by the top covers, is drawn. Near $s=s^*$ the band of leaves of types F and B descends towards the axis until it reaches the edges of the zone column, where its lowest leaves lie at about $r=10^{-4}$; inside this column the fold reaches the axis at $p^*$, where $\Db$ splits into the two nappes.}\label{fig:fold} \end{figure} \emph{The region functions.} The fold table is a floating-point table with $423$ nodes $s\in[0.5775,0.999]$. At each node it lists the radius of the fold at the angles $\varphi=0^\circ,1^\circ,\dots,360^\circ$, where one was found. Let $r_f^{\max}(s)$ and $r_f^{\min}(s)$ be the largest and the smallest of these radii, interpolated linearly in $s$ and constant beyond the ends of the table. A missing radius counts as $0$ in $r_f^{\max}$ and as $9$ in $r_f^{\min}$. Then \[ \rtop(s)=(1+2^{-40})\max\bigl(1.5\,r_f^{\max}(s),\ r_{\mathrm{fl}}(s)\bigr),\qquad \rax(s)=0.4\,(1+2^{-40})\min\bigl(r_f^{\min}(s),\ 0.3\,|s-\tilde s|\bigr). \] Here the floor $r_{\mathrm{fl}}(s)$ is $6.2\cdot10^{-4}$ for $s\in[0.7086181640625,\,0.7110595703125]$ and $0$ otherwise. The double $\tilde s=0.7097084911075526$ lies in the $s$-range of the zone column. In these formulas $0.4$, $0.3$ and $6.2\cdot10^{-4}$ denote the doubles nearest to them, which the programs use; the other constants are doubles. We chose the factors $1.5$, $0.4$ and $0.3$ to split the work between the covers. This choice affects whether the certificates succeed, not their validity: off the zone column the inclusion argument of Section~\ref{sec:inclusion} works for any positive continuous $\rax$ for which the roots of the fold-core covers contain the regions that it defines. The axis and lower axis covers, which cover $r\le\rax$, have leaves of types M and X only, so their certificates can succeed only if $J<0$ at all physical points with $s\le\sH$ and $r\le\rax$ off the zone column. Floating-point rounding in the programs that build the covers cannot invalidate an inclusion, since the exact check of Section~\ref{sec:checklist} repeats in rational arithmetic all comparisons of boxes with regions; an inaccurate table could only make certificates fail. \subsection{Leaf types}\label{sec:types} Each leaf of a fold-core cover is a box of its chart's subdivision tree. Except for the leaves of type X excluded by the $\alpha$-test and the leaves of type U, each leaf is resolved on a ball that contains it. The type of a leaf states what is certified on its box (Table~\ref{tab:types}). In the table, ``physical point'' means a physical point of the box and ``point of $\Sigma$'' a physical point of the box with $J=0$. The types F and B use \emph{projected enclosures}. For a box and constants $\hat c_1$, $\hat c_2$, $\hat c_3$ that we choose at its centre, these are enclosures over the box of $T_\ell-\hat c_\ell\Jt$, $\ell=1,2,3$, which equal $T_\ell$ where $\Jt=0$. \begin{table}[ht] \centering\small \begin{tabular}{@{}l>{\raggedright\arraybackslash}p{2.65in}>{\raggedright\arraybackslash}p{2.65in}@{}} \toprule type & certified on the box & consequence\\ \midrule M & $\Jt<0$ & $J<0$ at all physical points\\\addlinespace[2pt] P & $\Jt>0$ & $J>0$ at all physical points\\\addlinespace[2pt] F & projected $T_1>0$, $T_2<0$ and $T_3<0$, plus $P$ or $Q$ strictly signed in the umbilic cover & at all points of $\Sigma$: $T_1>0$, $T_2<0$, $T_3<0$\\\addlinespace[2pt] B & band certificate (below): on the cell, projected $T_1>0$ and $T_2<0$, and the bracket of Lemma~\ref{lem:band} at most $\beta_C<0$; on the mirror face, $\Jm\ne0$, $(P,Q)\ne0$ and $T_1>0$ & at all points of $\Sigma$: $T_1>0$, $T_2<0$; off the mirror $T_3<0$, with the bound \eqref{eq:bandquant}; on the mirror $\Jm\ne0$ and $T_3=0$\\\addlinespace[2pt] X & $K>0$ on the resolved box, or the $\alpha$-test on the box & no physical point\\\addlinespace[2pt] U & no property & lies in the umbilic ball\\ \bottomrule \end{tabular} \par\vspace{6pt} \caption{The types of the leaves of the fold-core covers.}\label{tab:types} \end{table} Further conditions depend on the chart. \begin{itemize}[leftmargin=2em] \item Charts $0$ and $4$ have leaves of types M and X only. \item Chart $2$: all leaves have $K<0$, and none is of type X. \end{itemize} \emph{The band certificate} (charts $1$ and $3$). The cell of a band certificate is a ball that contains the leaf's box and has exactly one mirror angle $\varphi_m$ in its $\varphi$-range. It certifies that $\Jt<0$ on the lower $r$-face of the cell and $\Jt>0$ on the upper one. Then $\Jt$ has a zero on each $r$-segment of the cell. The segments on the mirror provide the zeros required by Lemma~\ref{lem:band}. On the cell it certifies projected $T_1>0$ and $T_2<0$ and finite enclosures of $\partial_\varphi^2T_3$ and $\partial_\varphi^2\Jt$. On the mirror face it certifies that $\Jm$ is strictly signed, that $P$ or $Q$ is strictly signed, and that $T_1>0$. Finally, it certifies a negative upper bound $\beta_C$ of the bracket of Lemma~\ref{lem:band}. The program that builds the cover encloses the bracket with outward rounding; the separately written checking program of Section~\ref{sec:checklist} recomputes its largest value over the corners of the enclosures in exact rational arithmetic. Lemma~\ref{lem:band} then gives \eqref{eq:bandquant} with $\beta=\beta_C$ for the certified quantities of the chart. The version for chart~$2$ uses $\psi$-faces and $\partial_\psi(\Jt/\varrho^2)$. The band certificate is used only on the mirror $\varphi=90^\circ$ for $ss^*$, and for the umbilic cover only at the points with $\varrho>0$ (Proposition~\ref{prop:cert}(h)). Of the $2334$ leaves of type B of the core cover, $980$ lie below $s^*$ and $1354$ above it. All $25$ leaves of type B of the lower core cover lie below $s^*$ and all $27$ of the top core cover above it; the umbilic cover has one of each kind. \emph{The other covers.} In the bulk, corner and fin covers, a leaf of type P certifies $J>0$ at all physical points of the chart's region over the box, in the charts of Appendix~\ref{app:charts} together with the uniqueness of the zero of the Krawczyk step. A leaf of type X certifies that no physical point of the region lies over the box. A leaf of type D is deferred to the fold-core covers. In the bulk cover these are $32$ boxes near the umbilic that lie in the core region. In the corner cover at $(1,1,1)$ they are boxes in $\hat r<0.184$, whose points routed to this cover in Section~\ref{sec:inclusion} lie in the top covers. \subsection{Inclusion}\label{sec:inclusion} We glue the covers by the three routing statements of Lemma~\ref{lem:routes}, whose constants we check in exact arithmetic. Let $\Tfin=1.9499999995$, a value that satisfies the inequalities used in Lemma~\ref{lem:routes}(a). \begin{lemma}\label{lem:routes} Let $a\in W$ be physical. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item \textup{(Fin lemma.)} If $a_1+a_2\ge\Tfin$ and $a_3\le0.9$, then $-K\le0.08$ and $\theta_1\in[\pi/2,\pi)$. If also $a_3\ge0.125$, then $u=(-K,a_3,\theta_1)$ lies in the domain of the fin cover. \item \textup{(Top route.)} If $s\ge\sH$, then $1-a_3<3\sigma\le3/32<0.1$. If $a_3\ge0.9$, then $1-a_3\le0.1$. In both cases $a$ lies in the domain of the corner cover at $(1,1,1)$. \item \textup{(From the corner at $(1,1,1)$ to the top charts.)} Let $\delta=2-\Tfin$. If $a_1+a_2\ge\Tfin$ and $a$ lies in a leaf of type D of the corner cover at $(1,1,1)$, then $\sigma<\delta/(2-0.184\sqrt6/3)\le1/32$. \end{enumerate} \end{lemma} \begin{proof} (a) As $a_1\ge a_2$ and $a_1<1$, we have $a_1\ge\Tfin/2$ and $a_2>\Tfin-1$. From the first, $0<-K=w_1(1-q_1)0$. Then $R_3=q_3^{-2/3}\le q_{lo}^{-2/3}\le\Tfin^2/2\le a_1^2+a_2^2$. Therefore $\cos\theta_3\ge0$, that is $\theta_3\le\pi/2$. As $\theta_2<\pi$, it follows that $\theta_1=2\pi-\theta_2-\theta_3\ge\pi/2$, while $\theta_1<\pi$ as $a$ is physical. (b) We have $1-a_3=\sigma+2y/\sqrt6$ and, by Lemma~\ref{lem:B1}, $y\le r<\sqrt6\,\sigma$. The other two coordinates of $\mathrm{CH}_{111}$ lie in $[0,1]$ by $a_1\ge a_2\ge a_3$. (c) Since the leaves of type D of this cover lie in $\hat r<0.184$ (Section~\ref{sec:checklist}), we have $y\le r<0.184\,\sigma$. Then $a_1+a_2=2s+2y/\sqrt6\ge\Tfin$ implies $2\sigma-\delta\le2y/\sqrt6<0.184\,\sigma\sqrt6/3$. \end{proof} With the exact inclusion check we verify the following statements, which together show the two coverage statements of Proposition~\ref{prop:cert}(b). \begin{itemize}[leftmargin=2em] \item $\frac120$, which is not stored with the cover. \item \emph{Exact inclusion.} We verify all statements of Section~\ref{sec:inclusion} in rational arithmetic. Where the irrational numbers $2^l$ (chart~$1$) and $\pi$ enter, we use rational bounds from Arb. The same check verifies the constants of Lemma~\ref{lem:routes}, the parameters stored with the covers, the signs of $\lax$ at $s_a$ and $s_b$, the inclusion of each leaf's box in its ball (for the leaves of type B, in its cell: check (3)), and the stored types. \item \emph{The level of the umbilic, the ends, the half-plane condition and the equal-mass check}: the checks behind Proposition~\ref{prop:cert}(c)--(g) below. \end{enumerate} In (3)--(5) the re-evaluations call the same compiled libraries as the programs that built the covers, so they test these programs and the stored covers, not the formulas that the libraries evaluate (see Data and code availability). \subsection{Summary}\label{sec:certsummary} \begin{proposition}\label{prop:cert} The computations described in this section establish the following. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $\lax(s_a)>0>\lax(s_b)$, with $s_a$, $s_b$ as in Section~\ref{sec:axis}. \item Every leaf of the covers of Table~\ref{tab:covers} has the properties of Section~\ref{sec:types} for its type and chart. The leaves of the fold-core covers and the umbilic ball cover all points of the fold core in $W$, physical or not. Every physical point of $W$ outside the fold core lies in a leaf of type P of the bulk, corner or fin covers. \item The umbilic ball lies in $\Om$, and $K\le-0.8283$ on it. Every leaf of the umbilic cover spans the whole range $0\le\varrho\le\varrho_{\mathrm u}$. The leaves whose $\psi$-range contains $0$ or $\pi$ contain the axis points with $\varrho>0$, and they are of type M. The leaves whose $\psi$-range contains $\pi/2$ contain the points of the plane $s=s^*$ with $\varrho>0$, and they are of type P. \item Every leaf of type M, P, F or B of the fold-core covers other than the umbilic cover is resolved and has finite enclosures of $K$ and $\hA$ (of $K/\sigma$ and $A-\log\sigma$ in charts $3$ and $4$). \item $J>0$ at every physical point with $s=s^*$ other than $p^*$. \item Let $u_L=(\cos75^\circ,\sin75^\circ)$ and $u_U=(\cos220^\circ,\sin220^\circ)$. At every point of $\Sigma\cap W$, $u_L\cdot(P,Q)>0$ if $s0$ if $s>s^*$. \item The point $a=s_{eq}(1,1,1)$ has $K<0$ and $J<0$. There is a physical point $a_{iso}$ on the mirror $\varphi=90^\circ$, approximately $(0.73904,0.73904,0.72291)$, with $A=Q=0$ and $J>0$. \item For every leaf of type B one of two cases holds. Either the points with $\varrho>0$ of its box and of its cell lie in $\{ss^*\}$ and $30^\circ$ is the only mirror angle in these ranges. The cells of the two leaves of type B of the umbilic cover span $0\le\varrho\le\varrho_{\mathrm u}$. One has its $\psi$-range in $(\pi/2,\pi)$ and the mirror angle $90^\circ$. The other has its $\psi$-range in $(0,\pi/2)$ and the mirror angle $30^\circ$. \end{enumerate} \end{proposition} We indicate how (a) and (c)--(h) are obtained, item (b) being the content of Sections~\ref{sec:balls}--\ref{sec:inclusion}. (a) Arb enclosures of $\lax$ at the two doubles have the stated signs. (c) An evaluation over $256$ boxes that cover the umbilic ball in chart~$0$ is resolved and shows that $K\le-0.8283$. We read off the ranges in $\varrho$ and the types of the leaves of the umbilic cover from the stored cover. (d) We re-evaluate all leaves of type M, P, F or B of the fold-core covers other than the umbilic cover (checks (4) and (7)) and obtain the stated result. (e) In the core cover, the leaves that meet $s=s^*$ are of types P and F. Re-evaluated on the pieces that meet $[s_a,s_b]$, the F leaves have $\Jt>0$. The axis, lower core and lower axis covers have no leaves there, the top covers lie in $s\ge\sH$, the leaves of type U lie in the umbilic ball, and the leaves of the umbilic cover that meet $\psi=\pi/2$ are of type P. Outside the fold core, $J>0$ by (b). (f) All leaves of type F or B of the core, lower core, top core and umbilic covers are re-evaluated, split into pieces where necessary. Each piece either has $u\cdot(P,Q)>0$ with the vector $u$ of its nappe, or it has $\Jt$ of one sign or $K>0$. In the last two cases it contains no point of $\Sigma$. The pieces that meet $s=s^*$ are settled by the signs of $\Jt$ or $K$ alone. (g) On a box around $s_{eq}(1,1,1)$ the enclosures show $K<0$ and $\Jt\in[-4.06572,-4.06571]$. The enclosure of $A$ contains $0$, in agreement with Lemma~\ref{lem:axis}(c). On the mirror $P=0$. Let $z_0\approx(0.7336623572,\,0.0131679438)$ be a floating-point zero of $(A,Q)$ in the coordinates $(s,r)$ of the mirror. Let $v_1\approx(-0.0962865,\,-0.0430095)$ and $v_2\approx(0.0817315,\,1.5838743)$ be the columns of the inverse of a floating-point Jacobian matrix of $(A,Q)$ near $z_0$. On the parallelogram $\{z_0+t_1v_1+t_2v_2:\ |t_1|,|t_2|\le10^{-7}\}$ the enclosures show $A<0$ on the side $t_1=-10^{-7}$, $A>0$ on $t_1=10^{-7}$, $Q<0$ on $t_2=-10^{-7}$ and $Q>0$ on $t_2=10^{-7}$. The Poincaré--Miranda theorem \cite{Mir40,Kul97} then yields a zero of $(A,Q)$ in the parallelogram. On it $\Jt\in[12.0429,12.0438]$ and $K<0$. (h) We compare the balls of all band certificates with the mirror angles and with $[s_a,s_b]$, in chart~$2$ with $\psi=\pi/2$. The comparison is in exact rational arithmetic with Arb enclosures of $\pi$. In charts $1$ and $3$ each such ball lies in $ss_b$. Moreover $s_a\le s^*\le s_b$. The ranges in $\varrho$ of the two cells of the umbilic cover are read off from the stored cover. \section{The count at regular values}\label{sec:thm1} In this section we prove the following proposition, the first step towards Theorem~\ref{thm:count}, together with the injectivity of the mass map on $\Db$, on which the later sections build. \begin{proposition}[the count at regular values]\label{prop:regcount} Let $m$ be positive masses and $i\in\{1,2,3,4\}$. Then $1\le c_i(m)\le4$. If $\mu^{(i)}(m)$ is a regular value of the mass map $F_i$, then $c_i(m)\in\{2,4\}$. The critical values of $F_i$ form a closed null subset of $\R^3$. \end{proposition} We prove it for $i=4$ and write $F=F_4$. The other cases follow by relabelling the bodies. Section~\ref{sec:proper} proves properness, and Section~\ref{sec:topology} collects three topological lemmas. Sections~\ref{sec:rays}--\ref{sec:injective} prove that $F$ is injective on $\Db$ and determine the slices $F(\Db)\cap\{A=c\}$. Section~\ref{sec:restricted} computes the preimages of one regular value through the restricted problem, and Section~\ref{sec:counting} carries this count to all regular values and proves Proposition~\ref{prop:regcount}. The statements about $W$ in Proposition~\ref{prop:cert} extend to $\Om$ by $\Sym$-equivariance. \subsection{Properness}\label{sec:proper} For a configuration $x$ and masses $m$ let $U(x)=\sum_{iR(\vartheta)\}. \end{gather*} \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $\R^2$ is the disjoint union of $\mathrm{In}(R)$, $C(R)$ and $\mathrm{Out}(R)$. The sets $\mathrm{In}(R)$ and $\mathrm{Out}(R)$ are open, and $C(R)$ is compact. \item $\mathrm{In}(R)$ is bounded and star-shaped about $0$, hence path-connected. \item $\mathrm{Out}(R)$ is unbounded and path-connected, and $tw\in\mathrm{Out}(R)$ for all $w\in\mathrm{Out}(R)$ and $t\ge1$. \item Every point of $C(R)$ is a limit of points of $\mathrm{In}(R)$ and of points of $\mathrm{Out}(R)$. \end{enumerate} \end{lemma} \begin{proof} Each $w\ne0$ is $\rho e^{i\vartheta}$ for exactly one pair $(\rho,\vartheta)$ with $\rho>0$, which gives the partition. The function $\rho e^{i\vartheta}\mapsto\rho-R(\vartheta)$ is continuous on $\R^2\setminus\{0\}$; the sets $\mathrm{Out}(R)$ and $\mathrm{In}(R)\setminus\{0\}$ are the open sets where it is positive and negative. The disc of radius $\min R>0$ lies in $\mathrm{In}(R)$, so $\mathrm{In}(R)$ is open. The set $C(R)$ is the image of the compact $S^1$. If $\rho e^{i\vartheta}\in\mathrm{In}(R)$ and $t\in[0,1]$, then $t\rho\max(\rho,\max R)$, the segment from $\rho e^{i\vartheta}$ to $\lambda e^{i\vartheta}$ lies in $\mathrm{Out}(R)$, and so does the circle of radius $\lambda$. This joins any two points of $\mathrm{Out}(R)$. Finally $R(\vartheta)e^{i\vartheta}$ is the limit of $(R(\vartheta)\pm\epsilon)e^{i\vartheta}$ as $\epsilon\downarrow0$. \end{proof} \begin{lemma}[fibre counts]\label{lem:fibres} Let $X$ be a Hausdorff space, $f:X\to\R^m$ a continuous proper map and $Y\subset\R^m$ an open set. Suppose that each $x\in f^{-1}(Y)$ has an open neighbourhood $U$ such that $f(U)$ is open and $f|_U:U\to f(U)$ is a homeomorphism. Then for each $y\in Y$ the fibre $f^{-1}(y)=\{x_1,\dots,x_k\}$ is finite. Given pairwise disjoint neighbourhoods $U_i\ni x_i$ of this kind, there is an open set $\mathcal V\subset Y$ containing $y$ such that each $y'\in\mathcal V$ has exactly one preimage in each $U_i$ and none outside $U_1\cup\dots\cup U_k$. In particular the number of preimages is locally constant on $Y$, hence constant on each connected subset of $Y$. \end{lemma} \begin{proof} The fibre is compact, since $f$ is proper. It is discrete, since $f$ is injective on each $U$. Hence it is finite. Pairwise disjoint neighbourhoods $U_i$ exist since $X$ is Hausdorff. Let $B\subset Y$ be a closed ball around $y$. The set $X_B=f^{-1}(B)\setminus(U_1\cup\dots\cup U_k)$ is compact; $f(X_B)$ does not contain $y$. The open set $\mathcal V=\operatorname{int}B\cap f(U_1)\cap\dots\cap f(U_k)\setminus f(X_B)$ contains $y$ and has the stated property. \end{proof} \begin{lemma}[planar covering lemma]\label{lem:planarcover} Let $X$ be a compact Hausdorff space, $X^\circ\subset X$ an open subset and $\partial X=X\setminus X^\circ$, and let $f:X\to\R^2$ be continuous. Let $R:S^1\to(0,\infty)$ be continuous. Suppose that \begin{enumerate}[label=\textup{(\roman*)},leftmargin=2.5em] \item each $x\in X^\circ$ has an open neighbourhood $U\subset X^\circ$ such that $f(U)$ is open and $f|_U:U\to f(U)$ is a homeomorphism, and \item $f(\partial X)\subset C(R)$. \end{enumerate} Then the following hold. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $f(X^\circ)\subset\mathrm{In}(R)$. In particular $f^{-1}(\mathrm{Out}(R))=\emptyset$ and $f^{-1}(C(R))=\partial X$. \item The number of preimages of $y$ is finite and does not depend on $y\in\mathrm{In}(R)$. \item Suppose moreover that \textup{(iii)} $f$ maps $\partial X$ bijectively onto $C(R)$, and that \textup{(iv)} some point of $\mathrm{In}(R)$ has exactly one preimage. Then $f$ is a homeomorphism of $X$ onto $\mathrm{In}(R)\cup C(R)$, which maps $X^\circ$ onto $\mathrm{In}(R)$. \end{enumerate} \end{lemma} \begin{proof} The set $Y=\R^2\setminus C(R)=\mathrm{In}(R)\cup\mathrm{Out}(R)$ is open. By (ii), $f^{-1}(Y)\subset X^\circ$. Since $X$ is compact, $f$ is proper. By (i), every point of $f^{-1}(Y)\subset X^\circ$ has an open neighbourhood that $f$ maps homeomorphically onto an open set, so Lemma~\ref{lem:fibres} applies to $f$ and $Y$. Thus $n(y)=\#f^{-1}(y)$ is finite and locally constant on $Y$. It is therefore constant on the path-connected sets $\mathrm{In}(R)$ and $\mathrm{Out}(R)$ (Lemma~\ref{lem:polar}). As $f(X)$ is compact and $\mathrm{Out}(R)$ is unbounded, $n=0$ at some point of $\mathrm{Out}(R)$, hence on all of $\mathrm{Out}(R)$. Suppose that a point $x\in X^\circ$ had $f(x)\in C(R)$. With $U$ as in (i), $f(U)$ would be an open neighbourhood of $f(x)$. It contains points of $\mathrm{Out}(R)$ by Lemma~\ref{lem:polar}(d). These would have preimages in $U$, which is impossible. Therefore $f(X^\circ)\subset\mathrm{In}(R)$, which proves (a) and (b). Under (iv), $n=1$ on $\mathrm{In}(R)$, so $f$ maps $X^\circ=f^{-1}(\mathrm{In}(R))$ bijectively onto $\mathrm{In}(R)$. Under (iii) it maps $\partial X$ bijectively onto $C(R)$. As $\mathrm{In}(R)\cap C(R)=\emptyset$, $f$ is then a continuous bijection of the compact space $X$ onto the Hausdorff space $\mathrm{In}(R)\cup C(R)$, hence a homeomorphism. \end{proof} \subsection{Rays}\label{sec:rays} Sections~\ref{sec:rays}--\ref{sec:ends} derive from the certificates the shape of $\Db$: it meets every ray from the axis in an initial segment, the umbilic splits it into two nappes, and we determine the limit points of these nappes. Sections~\ref{sec:levels} and~\ref{sec:foldcurves} use these facts, the signs of $T_1$, $T_2$ and $T_3$ on the fold and the half-plane condition to describe the level sets of $A$ on the nappes and the fold curves $\Gamma_c$ in them. Section~\ref{sec:injective} then counts the sheets of $G$ over each level set at one point near the fold. We now study $\Db$ along the rays from the axis. For $s\in(\frac12,1)$ and $\varphi\in[30^\circ,90^\circ]$, the \emph{ray} $\{a(s,r,\varphi):r\ge0\}$ meets the part $FC(s)$ of the fold core in a segment $\{0\le r\le r_{\max}(s)\}$. \begin{lemma}\label{lem:raysfacts} \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $J>0$ at every physical point of $W$ outside the fold core. \item On the axis, $J<0$ at the physical points other than $p^*$, while $J(p^*)=0$. \item For each ray, the physical points of $FC(s)$ on the ray form an initial segment of $FC(s)\cap\mathrm{ray}$. \item Every physical point of $W$ with $J=0$, other than $p^*$, has $T_1=\partial_r\Jt>0$ and lies in a leaf of type F or B. In particular, for $s\ne s^*$, $J$ has at most one zero on the physical part of $FC(s)\cap\mathrm{ray}$, and such a zero is a transverse crossing from $J<0$ to $J>0$. \end{enumerate} \end{lemma} \begin{proof} (a) By Proposition~\ref{prop:cert}(b), every physical point of $W$ outside the fold core lies in a leaf of type P of the bulk, corner or fin covers, and such a leaf certifies $J>0$ there (Section~\ref{sec:types}). (b) This is the last assertion of Proposition~\ref{prop:ax}. The covers certify it independently. The axis lies in the regions of the covers of charts $0$ and $4$ (the lower axis, axis and top axis covers), whose leaves are of types M and X. On the zone column it lies in the umbilic ball, where the axis points with $\varrho>0$ lie in leaves of type M of the umbilic cover (Proposition~\ref{prop:cert}(c)). Since the quantity certified in chart~$2$ is $\Jt/\varrho^2$, these leaves give $J<0$ at the axis points with $\varrho>0$. Since a physical axis point lies in none of the leaves of type X, the covers imply $J<0$ there unless it is $p^*$. (c) We argue by contradiction and suppose that a physical point $a(r_2)\in FC(s)$ lies beyond a non-physical point $a(r_1)\in FC(s)$, $r_10$, and Lemma~\ref{lem:convex}(b) shows that the points $a(r)$ with $r>r_0$ close to $r_0$ are not physical, against the choice of $r_0$. (d) By (a) and Proposition~\ref{prop:cert}(b), a physical point of $W$ with $J=0$ lies in the fold core, hence in a leaf of a fold-core cover or in the umbilic ball. We go through the types of leaves. The leaves of types M and P have $J\ne0$ at their physical points, those of type X contain none, and the leaves of type U lie in the umbilic ball. This ball is tiled by the leaves of the umbilic cover, of which those of types M and P have $\Jt/\varrho^2\ne0$. Unless the point is $p^*$, it lies in a leaf of type F or B. At such a point $T_1=\partial_r\Jt>0$, also in charts $2$ and $3$, where $T_1$ is the value in chart~$1$ multiplied by a positive factor. For $s\ne s^*$, each zero of $J$ on the physical part of $FC(s)\cap\mathrm{ray}$ is then a transverse crossing from $J<0$ to $J>0$. Since this physical part is an interval by (c), there is at most one such zero. \end{proof} Let $\cD=\{J<0\}\subset\Om$ and $\Db=\{J\le0\}\subset\Om$. Then $\Db$ is the closure of $\cD$ in $\Om$. Indeed, $\partial_r\Jt>0$ at all zeros of $J$ other than $p^*$ (Lemma~\ref{lem:raysfacts}(d), extended to $\Om$ in Lemma~\ref{lem:foldsigns}), and $p^*$ is a limit of axis points with $J<0$ by Lemma~\ref{lem:raysfacts}(b). \begin{lemma}\label{lem:rays} For $s\in(1/\sqrt3,1)\setminus\{s^*\}$, on each ray at level $s$ either $\Db\cap\mathrm{ray}=\{0\le r\le r_f\}$ with $J(a(r_f))=0$, or $\Db\cap\mathrm{ray}=\{0\le r0$ by Lemma~\ref{lem:raysfacts}(a). If $J$ has a zero $r_f$ on $I$, then $\Db\cap\mathrm{ray}=\{0\le r\le r_f\}$. Otherwise $J<0$ on $I$. If $I$ were the whole segment $FC(s)\cap\mathrm{ray}$, then, since $\Om$ is open, the points just beyond it would be physical points outside $FC(s)$. For $s\le\sB$ there are no such points, by Lemma~\ref{lem:B1}. For $s\ge\sB$ they would have $J>0$ by Lemma~\ref{lem:raysfacts}(a), against the continuity of $J$. Therefore $I=\{0\le r0$, and $\Sigma\cap\mathrm{ray}(s,\varphi)$ is the single point $a(s,r_f,\varphi)$. \item $s<2/3$ and $\Sigma\cap\mathrm{ray}(s,\varphi)=\emptyset$. \end{enumerate} \end{corollary} \begin{proof} The group $\Sym$ preserves $s$, $\Db$ and $\Sigma$. For each $\varphi$ one of its elements maps $\mathrm{ray}(s,\varphi)$ onto a ray whose angle lies in $[30^\circ,90^\circ]$. So we may assume $\varphi\in[30^\circ,90^\circ]$. Each zero of $J$ on the ray is a transverse crossing from $J<0$ to $J>0$, by Lemma~\ref{lem:raysfacts}(d). Such a zero lies in $\Sigma\subset\Db$, but the points just beyond it lie outside $\Db$. As $\Db\cap\mathrm{ray}(s,\varphi)$ is an interval (Lemma~\ref{lem:rays}), the zero is its right end. In the first case of Lemma~\ref{lem:rays} this yields (R1). Here $r_f>0$, since $J<0$ on the axis (Lemma~\ref{lem:raysfacts}(b)). In the second case the interval $\{0\le r0$ and $T_2<0$. At every point of $\Sigma\cap W$ off the two mirrors of $W$, $T_3<0$. \end{lemma} \begin{proof} By Lemma~\ref{lem:raysfacts}(d), each point of $\Sigma\cap W$ other than $p^*$ lies in a leaf of type F or B. Table~\ref{tab:types} and Lemma~\ref{lem:band} show that $T_1>0$ and $T_2<0$ at the points of $\Sigma$ in such a leaf and that $T_3<0$ at those off the mirrors. In charts $2$ and $3$ the certified quantities are positive multiples of $T_1$, $T_2$ and $T_3$ at these points (Sections~\ref{sec:balls} and~\ref{sec:charts}). The group $\Sym$ fixes $s$ and acts on $(x,y)$ by orthogonal maps. It therefore preserves $r$ and maps $e_s$ and $e_r$ at a point to $e_s$ and $e_r$ at the image point. As $A$, $K$ and $\Jt$ are invariant, so are $T_1=\partial_r\Jt$ and $T_2=\Av_s(\nabla\Jt)_r-\Av_r(\nabla\Jt)_s$. Each point of $\Om$ is the image of a point of $W$. \end{proof} \subsection{Nappes}\label{sec:nappes} We split $\Db$ at $p^*$: by Proposition~\ref{prop:cert}(e), $\Db\cap\{s=s^*\}=\{p^*\}$, and \[ \Db=\Db_L\sqcup\{p^*\}\sqcup\Db_U,\qquad \Db_L=\Db\cap\{ss^*\}. \] We call $\Db_L$ and $\Db_U$ the lower and upper \emph{nappes}. Put $\cD_L=\cD\cap\Db_L$, $\cD_U=\cD\cap\Db_U$, $\Sigma_L=\Sigma\cap\Db_L$ and $\Sigma_U=\Sigma\cap\Db_U$. By Lemmas~\ref{lem:axis}(b) and~\ref{lem:raysfacts}(b), the axis points $s(1,1,1)$ with $1/\sqrt30\}$. \begin{lemma}\label{lem:ends} If $\bar a\in\R^3$ is a limit of points $a^{(n)}\in\Db_L$ with $\bar a\notin\Db_L$, then either $\bar a=p^*$ and $A(a^{(n)})\to A^*$, or $K(\bar a)=0$, $s(\bar a)<2/3$ and $A(a^{(n)})\to+\infty$. If $\bar a$ is a limit of points $a^{(n)}\in\Db_U$ with $\bar a\notin\Db_U$, then either $\bar a=p^*$ and $A(a^{(n)})\to A^*$, or $\bar a$ has $\sigma=0$ in chart $3$ or $4$ and $A(a^{(n)})\to-\infty$. \end{lemma} \begin{proof} We treat $\Db_L$ first and let $a^{(n)}\in\Db_L$. If $\bar a\in\Om$, then $\bar a\in\Db$ ($\Db$ is closed in $\Om$) and $s(\bar a)=s^*$ ($s(\bar a)\le s^*$ and $\bar a\notin\Db_L$). Then $\bar a=p^*$ and $A(a^{(n)})\to A^*$. If $\bar a\notin\Om$, then $\bar a$ must lie in a leaf of $\cU$ outside the umbilic ball, since this ball is contained in $\Om$. From $s(\bar a)\le s^*<\sH$ we get $\sigma(\bar a)>0$. Hence the solution of Lemma~\ref{lem:angles} exists at $\bar a$ with $\theta\in(0,\pi)^3$ and $00$, the argument above shows that $K(\bar a)=0$ and $s(\bar a)<2/3$, which is impossible: $s(\bar a)\ge s^*>2/3$. The remaining limits must have $\sigma=0$ in chart $3$ or $4$. There $A-\log\sigma$ is finite and continuous up to $\sigma=0$; hence $A=(A-\log\sigma)+\log\sigma\to-\infty$. \end{proof} \subsection{The levels of \texorpdfstring{$A$}{A} on the nappes}\label{sec:levels} We put $\Phi_c=\Db_L\cap A^{-1}(c)$ for $c>A^*$ and $\Phi_c=\Db_U\cap A^{-1}(c)$ for $cA^*$ on $\Db_L$ and $A0$, since $p^*$ is the only point of $\Sigma$ on the axis. Since $T_1(a)>0$ and $T_2(a)<0$ (Lemma~\ref{lem:foldsigns}), Lemma~\ref{lem:foldformulas}(b) shows that the fold is a graph $r=r_f(s,\varphi)$ near $a$ and that $t\mapsto A(s+t,r_f(s+t,\varphi),\varphi)$ has the derivative $T_2/((-K)T_1)<0$ at $t=0$. For small $|t|$ these points lie in $\Sigma\cap\{s0$ from $p^*$, lies in one nappe and converges in $\cU$ to some $\bar a\ne p^*$. If the nappe is $\Db_L$, then $\bar a\notin\Db_L$, since $A(\bar a)=A^*$ would contradict (a), and Lemma~\ref{lem:ends} gives $A(a_n)\to+\infty$. For $\Db_U$ it gives $A(a_n)\to-\infty$. Both contradict $A(a_n)\to A^*$. \end{proof} \begin{corollary}\label{cor:levels} For every compact interval $I\subset\R$, the set $\Db\cap A^{-1}(I)$ is compact, and $G$ is bounded on it. Moreover $\Db\cap A^{-1}(c)=\Phi_c$, $\cD\cap A^{-1}(c)=\Phi_c^\circ$ and $\Sigma\cap A^{-1}(c)=\Gamma_c$ for $c\ne A^*$, and $\Db\cap A^{-1}(A^*)=\{p^*\}$. In particular $\Phi_c$ is compact for $c\ne A^*$. \end{corollary} \begin{proof} The identities follow from Lemma~\ref{lem:levels}(a), since $A(p^*)=A^*$. Let $a_n\in\Db\cap A^{-1}(I)$, and pass to a subsequence with $A(a_n)\to c\in I$. If $c>A^*$, we choose $\epsilon>0$ with $c-\epsilon>A^*$. Eventually $a_n$ lies in $\Db_L\cap A^{-1}[c-\epsilon,c+\epsilon]$, which is compact by Lemma~\ref{lem:levels}(b). The case $c0\}$ be the open half-plane of angle $\varphi$ bounded by the axis. \begin{lemma}\label{lem:foldcurve} Let $\varphi\in S^1$. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item There are $s_{\min}(\varphi)\in[1/\sqrt3,2/3]$ and a $C^1$ function $r_f:(s_{\min}(\varphi),s^*)\to(0,\infty)$ such that $\Sigma_L\cap H_\varphi=\{a(s,r_f(s),\varphi):s_{\min}(\varphi)1/\sqrt3$ (Lemma~\ref{lem:fermat}), $\Sigma_L\cap H_\varphi$ consists of the points $a(s,r_f(s),\varphi)$ with $s\in\mathsf S_\varphi$. By Corollary~\ref{cor:dichotomy}, $(2/3,s^*)\subset\mathsf S_\varphi$, since case (R2) needs $s<2/3$. Here $s^*>2/3$ because $s^{*3}=3/(6\sqrt3-2)>8/27$ (Proposition~\ref{prop:ax}). Let $s_1\in\mathsf S_\varphi$. The point $q_1=a(s_1,r_f(s_1),\varphi)$ lies in $\Sigma\setminus\{p^*\}$, so $\partial_r\Jt(q_1)=T_1(q_1)>0$ by Lemma~\ref{lem:foldsigns}. The implicit function theorem solves $\Jt(a(s,r,\varphi))=0$ near $q_1$ by a $C^1$ function $r=\tilde r(s)$ of $s$ near $s_1$. The points $a(s,\tilde r(s),\varphi)$ are physical, since $\Om$ is open. They lie in $\Sigma$ by Lemma~\ref{lem:foldformulas}(a). So $s\in\mathsf S_\varphi$ and $r_f(s)=\tilde r(s)$ for $s$ near $s_1$. Thus $\mathsf S_\varphi$ is open and $r_f$ is $C^1$. By Lemmas~\ref{lem:foldformulas}(b) and~\ref{lem:foldsigns}, $\alpha'=T_2/((-K)T_1)<0$ on $\mathsf S_\varphi$. Let $(s_-,s_+)$ be a component of $\mathsf S_\varphi$, and let $s_n\in(s_-,s_+)$ tend to $s_+$ or to $s_-$. The points $q_n=a(s_n,r_f(s_n),\varphi)$ lie in $\Db_L$. A subsequence converges to some $\bar q\in\cU$. Suppose that $\bar q\in\Db_L$. Then $\bar q\in\Sigma$, since $\Sigma$ is closed in $\Om$. It is not on the axis, because $s(\bar q)0$. The map $\gamma_c:S^1\to\Gamma_c$ is a homeomorphism, with inverse $\varphi|_{\Gamma_c}$. \end{proposition} \begin{proof} Let $c>A^*$. Then $\Gamma_c=\Sigma_L\cap A^{-1}(c)$, a set that does not meet the axis. By Lemma~\ref{lem:foldcurve}(a), $\alpha$ is a continuous, strictly decreasing bijection of $(s_{\min}(\varphi),s^*)$ onto $(A^*,\infty)$, which yields the existence and the uniqueness of $\gamma_c(\varphi)$. At $\gamma_c(\varphi_0)$ the system $(\Jt,A-c)=0$ in the unknowns $(s,r)$ has the Jacobian determinant $\partial_s\Jt\,\partial_rA-\partial_r\Jt\,\partial_sA=-T_2/(-K)\ne0$, so the implicit function theorem yields a $C^1$ solution $(s(\varphi),r(\varphi))$ for $\varphi$ near $\varphi_0$. The corresponding points are physical and lie in $\Sigma_L\cap A^{-1}(c)\cap H_\varphi$, so they are the points $\gamma_c(\varphi)$. Thus $s_c$ and $r_c$ are $C^1$. A continuous bijection of the compact space $S^1$ onto the Hausdorff space $\Gamma_c$ is a homeomorphism. For $cA^*$, the function $\theta_c$ maps the arc $\mathsf A_k$ increasingly and homeomorphically onto $\mathsf A_k$, and it fixes the endpoints. If $cA^*$. \emph{The arc $\mathsf A_0$.} For $\varphi\in\mathsf A_0$ the point $\gamma_c(\varphi)$ lies in $\Sigma\cap W$ and has $s0$ there by Proposition~\ref{prop:cert}(f). That is, $G$ lies in the open half-plane of the angles in $(-15^\circ,165^\circ)$. On this half-plane $\Theta$ has a continuous determination with values in $(-15^\circ,165^\circ)$. We write $\tilde\theta(\varphi)$ for its value at $G(\gamma_c(\varphi))$. At $\varphi=30^\circ$ we have $\Theta\in\{30^\circ,210^\circ\}$ (Section~\ref{sec:coords}), so $\tilde\theta(30^\circ)=30^\circ$. Likewise $\tilde\theta(90^\circ)=90^\circ$. Since $\Jt$ and $A$ are constant along $\gamma_c$, the tangent vector $\gamma_c'(\varphi)$ is orthogonal to $\nabla A$ and $\nabla\Jt$, hence a multiple of $v=\nabla A\times\nabla\Jt$. Because $\gamma_c$ is parametrized by $\varphi$, we have $d\varphi(\gamma_c'(\varphi))=1$. For $30^\circ<\varphi<90^\circ$, Lemma~\ref{lem:foldformulas}(c) gives \[ \tilde\theta'(\varphi)=\frac{d\Theta(v)}{d\varphi(v)}=\frac{r\,T_3}{(P^2+Q^2)\,T_2}>0, \] since $T_2<0$ and $T_3<0$ off the mirrors (Lemma~\ref{lem:foldsigns}). Thus $\tilde\theta$ increases strictly from $30^\circ$ to $90^\circ$; hence $\theta_c$ maps $\mathsf A_0$ increasingly and homeomorphically onto $\mathsf A_0$. \emph{The other arcs.} Let $g\in\Sym$ be the cyclic permutation that acts on $(x,y)$ as the rotation through $120^\circ$. It acts on $G$ by the same rotation (Section~\ref{sec:coords}) and preserves $s$, $A$ and $\Sigma$. It therefore maps $\Gamma_c\cap H_\varphi$ onto $\Gamma_c\cap H_{\varphi+120^\circ}$. The uniqueness in Proposition~\ref{prop:graph} then gives $g\gamma_c(\varphi)=\gamma_c(\varphi+120^\circ)$ and $\theta_c(\varphi+120^\circ)=\theta_c(\varphi)+120^\circ$. In the same way the transposition that fixes the mirror $\varphi=90^\circ$ gives $\theta_c(180^\circ-\varphi)=180^\circ-\theta_c(\varphi)$. The group generated by these two maps of $S^1$ carries $\mathsf A_0$ onto each $\mathsf A_k$. Under the rotation both $\varphi$ and $\Theta$ increase by $120^\circ$. Under the reflection both are replaced by $180^\circ$ minus themselves, which reverses both orders. In either case $\theta_c$ is again increasing on the image arc, maps it onto itself and fixes its endpoints. \emph{Consequences.} The arcs cover $S^1$ and overlap only at their endpoints, where $\theta_c$ is the identity. So $\theta_c$ is a continuous bijection of $S^1$, hence a homeomorphism. Proposition~\ref{prop:graph} then shows that $\Theta\circ G$ is a continuous bijection of the compact set $\Gamma_c$ onto $S^1$ and therefore a homeomorphism. Hence $R_c=|G|\circ(\Theta\circ G|_{\Gamma_c})^{-1}$ is continuous. It is positive since $G\ne0$ on $\Gamma_c$. Each $x\in\Gamma_c$ satisfies $G(x)=R_c(\Theta(G(x)))\,e^{i\Theta(G(x))}$. This shows that $G(\Gamma_c)=C(R_c)$ and that $G$ is injective on $\Gamma_c$. For $c0$ and a continuous function $M:(-\varepsilon_1,\varepsilon_1)\to(-\varepsilon_2,\varepsilon_2)$ with $M(0)=0$ such that the following holds for $|U|<\varepsilon_1$, $|V|<\varepsilon_2$ and $w=G(q)+Ue+Ve'$. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item If $VM(U)$, then $F^{-1}(c,w)\cap\mathcal N$ consists of two points, with $J<0$ at one of them and $J>0$ at the other. \end{enumerate} \end{lemma} \begin{proof} \emph{Step 1: independence.} At $q$ we have $K<0$ and, by Lemma~\ref{lem:foldsigns}, $T_2\ne0$. The $e_\varphi$-component of $v=\nabla A\times\nabla\Jt$ is $(\nabla A)_s(\nabla\Jt)_r-(\nabla A)_r(\nabla\Jt)_s=T_2/(-K)\ne0$. Thus $\nabla A(q)$ and $\nabla\Jt(q)$ are independent. Lemma~\ref{lem:foldformulas}(a) and the implicit function theorem show that the set $\Sigma\cap A^{-1}(c)=\{\Jt=0,\ A=c\}$ is a $C^1$ curve near $q$ whose tangent line at $q$ is $\R v(q)$. \emph{Step 2: rank.} By the definitions of Section~\ref{sec:quantities}, $T_3=\det[\hv;\Av;\nabla\Jt]=(-K)\,\hv\cdot v$, where $\hv\cdot v=P\,dQ(v)-Q\,dP(v)$. As $T_3(q)\ne0$, we get $dG(q)v\ne0$. Since $J(q)=0$, the restriction of $dG(q)$ to $\ker dA(q)$ is not injective, for otherwise $dF(q)=(dA,dG)(q)$ would be injective. As $v\in\ker dA(q)$ and $dG(q)v\ne0$, this restriction has rank $1$. Let $e$ be a unit vector that spans its image. \emph{Step 3: coordinates.} Put $u=e\cdot(G-G(q))$. Then $du(q)v=e\cdot dG(q)v\ne0=dA(q)v$, so $dA(q)$ and $du(q)$ are independent. We choose an affine function $\zeta$ of $a$ with $\zeta(q)=0$ and $d\zeta\notin\operatorname{span}(dA(q),du(q))$. By the inverse function theorem, $(A,u,\zeta)$ are coordinates on a connected open neighbourhood $\Omega_q\subset\Om$ of $q$, in which $q=(c,0,0)$. With $e'=e^\perp$ and $h=e'\cdot(G-G(q))$, the map $F$ reads $(A,u,\zeta)\mapsto(A,u,h(A,u,\zeta))$ in the target coordinates $(A,U,V)$. \emph{Step 4: the sign of $J$.} By the chain rule, $\partial_\zeta h=\det\partial(A,U,V)/\partial(A,u,\zeta)=\pm J\,D_0$, where $D_0=\det\partial(s,x,y)/\partial(A,u,\zeta)$ does not vanish on $\Omega_q$. Here we used $\det\partial(A,P,Q)/\partial(s,x,y)=J$ (proof of Lemma~\ref{lem:axis}(d)). It follows that $\Sigma\cap\Omega_q=\{\partial_\zeta h=0\}$ and that $\operatorname{sign}J=\epsilon_0\operatorname{sign}\partial_\zeta h$ on $\Omega_q$ for a constant $\epsilon_0\in\{1,-1\}$. \emph{Step 5: nondegeneracy.} Put $h_c(u,\zeta)=h(c,u,\zeta)$. At $q$, where $J=0$, we have $d(\partial_\zeta h)=\pm D_0\,dJ$ and $\nabla\Jt=(-K)\nabla J$. Step~1 shows that $dJ(q)$ is not a multiple of $dA(q)$, so $(\partial_u\partial_\zeta h_c,\partial_\zeta^2h_c)(0,0)\ne(0,0)$. Near $0$ the curve $\Sigma\cap A^{-1}(c)$ is $\{\partial_\zeta h_c=0\}$; its tangent at $0$ is spanned by $(du(v),d\zeta(v))$, which is not parallel to $\partial_\zeta$ since $du(v)\ne0$. If $\partial_\zeta^2h_c(0,0)$ vanished, then $\partial_u\partial_\zeta h_c(0,0)\ne0$, and the curve would be a graph $u=g_1(\zeta)$ with $g_1'(0)=0$, tangent to $\partial_\zeta$. Therefore $\partial_\zeta^2h_c(0,0)\ne0$. Replacing $e'$ by $-e'$, and $h$ by $-h$, we may assume $\partial_\zeta^2h_c(0,0)>0$. \emph{Step 6: one variable.} Given $\mathcal N_0$, we choose $\delta>0$ such that the closed coordinate box $\{|A-c|\le\delta,\ |u|\le\delta,\ |\zeta|\le\delta\}$ lies in $\mathcal N_0\cap\Omega_q$ and $\partial_\zeta^2h_c\ge\nu$ on $[-\delta,\delta]^2$ for some $\nu>0$. We choose $\varepsilon\in(0,\delta]$ with $|\partial_\zeta h_c(u,0)|\le\nu\delta/2$ for $|u|\le\varepsilon$. For $|u|\le\varepsilon$ the function $\partial_\zeta h_c(u,\cdot)$ increases strictly on $[-\delta,\delta]$, it is at most $-\nu\delta/2$ at $-\delta$ and at least $\nu\delta/2$ at $\delta$, and it has exactly one zero $\zeta^*(u)$, located in $[-\delta/2,\delta/2]$. The function $\zeta^*$ is continuous. We put $M(u)=h_c(u,\zeta^*(u))$, so that $M(0)=h_c(0,0)=0$. The function $h_c(u,\cdot)$ decreases strictly on $[-\delta,\zeta^*(u)]$ and increases strictly on $[\zeta^*(u),\delta]$. Moreover $h_c(u,\zeta)\ge M(u)+\frac\nu2(\zeta-\zeta^*(u))^2$, so $h_c(u,\pm\delta)\ge M(u)+\nu\delta^2/8$. We choose $\varepsilon_1\in(0,\varepsilon]$ with $|M(u)|<\nu\delta^2/16$ for $|u|<\varepsilon_1$. We put $\varepsilon_2=\nu\delta^2/16$ and $\mathcal N=\{|A-c|<\delta,\ |u|<\varepsilon,\ |\zeta|<\delta\}$. For $|U|<\varepsilon_1$ and $|V|<\varepsilon_2$ we have $VM(U)$. In the second case the solution is $\zeta^*(U)$, where $J=0$. In the third case one solution has $\partial_\zeta h_c<0$ and the other $\partial_\zeta h_c>0$, so $J$ has opposite signs there by Step~4. The preimages of $(c,w)$ in $\mathcal N$ are exactly the points $(c,U,\zeta)$ with these $\zeta$. \end{proof} \begin{lemma}\label{lem:onesheet} Let $c\ne A^*$. The map $f=G|_{\Phi_c}$ satisfies the hypotheses \textup{(i)--(iii)} of Lemma~\ref{lem:planarcover} with $X=\Phi_c$, $X^\circ=\Phi_c^\circ$, $\partial X=\Gamma_c$ and $R=R_c$. Some point of $\mathrm{In}(R_c)$ has exactly one preimage in $\Phi_c$. \end{lemma} \begin{proof} \emph{Hypothesis (i).} By Corollary~\ref{cor:levels}, $\Phi_c^\circ=\cD\cap A^{-1}(c)$, which is open in $\Phi_c$ since $\cD$ is open. For $x\in\Phi_c^\circ$, the inverse function theorem yields an open set $U\ni x$ in $\cD$ such that $F|_U$ is a homeomorphism onto an open set. Then $U\cap A^{-1}(c)$ is an open neighbourhood of $x$ in $\Phi_c$, contained in $\Phi_c^\circ$; $G$ maps it homeomorphically onto the open set $\{w:(c,w)\in F(U)\}$. \emph{Hypotheses (ii) and (iii)} hold by Proposition~\ref{prop:angle}. \emph{The base point.} By Lemma~\ref{lem:planarcover}(a), no point of $\Phi_c^\circ$ is mapped into $C(R_c)$. Let $q=\gamma_c(60^\circ)$, a fold point. Since $G(q)\in C(R_c)$ and $G$ is injective on $\Gamma_c$, the point $q$ is the only point of $\Phi_c$ that $G$ maps to $G(q)$. We apply Lemma~\ref{lem:foldnormal} at $q$ with $\mathcal N_0=\Om$. It yields $\mathcal N$, $\varepsilon_1$, $\varepsilon_2$ and $M$. The compact set $G(\Phi_c\setminus\mathcal N)$ does not contain $G(q)$, so $G(q)$ has a neighbourhood $Y_1$ that does not meet it. Take $y_0=G(q)+V_0e'\in Y_1$ with $0M(0)=0$, Lemma~\ref{lem:foldnormal}(c) shows that $F^{-1}(c,y_0)\cap\mathcal N=\{x_-,x_+\}$ with $J(x_-)<0A^*$ on $\Db_L$ and $A0$. Then $\Pi_c\circ G$ is a homeomorphism of $\Phi_c$ onto the closed unit disk, which maps $\Gamma_c$ onto the unit circle and $\Phi_c^\circ$ onto the open disk. In particular $\Phi_c$ is a closed disk with boundary circle $\Gamma_c$. \end{corollary} \begin{proof} Theorem~\ref{thm:inj}(b) shows that $G$ is a homeomorphism of $\Phi_c$ onto $\mathrm{In}(R_c)\cup C(R_c)$. The map $\Pi_c$ is a bijection onto the closed unit disk: its inverse is $\rho e^{i\vartheta}\mapsto\rho R_c(\vartheta)e^{i\vartheta}$. Both maps are continuous, because $R_c$ is continuous and $0<\min R_c\le\max R_c<\infty$. \end{proof} \input{frag/degree} \subsection{Counting}\label{sec:counting} For $\mu\in\R^3$ let $n_\pm(\mu)$ be the number of points of $F^{-1}(\mu)$ at which $\pm J>0$. The critical values of $F$ form the set $F(\Sigma)$; the other points of $\R^3$ are the regular values. We show that $n_+-n_-=2$ at all regular values and then count the preimages. The proof combines the injectivity of Section~\ref{sec:injective}, the base value of Section~\ref{sec:restricted} and the fold normal form at one fold point on each nappe. \begin{lemma}\label{lem:locconst} The set $\R^3\setminus F(\Sigma)$ of regular values is open, and $n_+$ and $n_-$ are locally constant on it. \end{lemma} \begin{proof} The set $F(\Sigma)$ is closed, since $\Sigma$ is closed in $\Om$ and the proper map $F$ is closed. Let $Y=\R^3\setminus F(\Sigma)$. The points of $F^{-1}(Y)$ have $J\ne0$, so by the inverse function theorem they have neighbourhoods $U$ on which $F$ is a homeomorphism onto an open set. We may assume that each $U$ is connected and that $J$ has one sign on it. Let $\mu\in Y$. Lemma~\ref{lem:fibres}, applied with $X=\Om$ and $f=F$, shows that the fibre $F^{-1}(\mu)=\{x_1,\dots,x_k\}$ is finite. For pairwise disjoint such neighbourhoods $U_i\ni x_i$ there is an open set $\mathcal V\ni\mu$ such that each $\mu'\in\mathcal V$ has exactly one preimage in each $U_i$ and no other preimage. This preimage has the sign of $J(x_i)$, so $n_\pm(\mu')=n_\pm(\mu)$. \end{proof} \begin{lemma}[fold crossing]\label{lem:foldcross} Let $q$ be a fold point and $c=A(q)$. Then $F^{-1}(F(q))=\{q,p_1,\dots,p_n\}$ is finite, and $J(p_j)>0$ for each $j$. Moreover $G(q)$ has an open neighbourhood $Y_2\subset\R^2$ such that $n_+(c,w)-n_-(c,w)=n$ for every $w\in Y_2$ for which $(c,w)$ is a regular value. \end{lemma} \begin{proof} Theorem~\ref{thm:inj}(a) shows that $q$ is the only point of the fibre in $\Db$. All other points have $J>0$. They are isolated in the fibre by the inverse function theorem. Lemma~\ref{lem:foldnormal}(b), applied with $\mathcal N_0=\Om$ and $(U,V)=(0,0)$, shows that $q$ is isolated in the fibre. The fibre is compact (Proposition~\ref{prop:proper}), hence finite. We choose pairwise disjoint open sets $\mathcal N_0\ni q$ and $\mathcal N_j\ni p_j$ such that $F|_{\mathcal N_j}$ is a homeomorphism onto an open set and $J>0$ on $\mathcal N_j$. Lemma~\ref{lem:foldnormal} with this $\mathcal N_0$ yields $\mathcal N\subset\mathcal N_0$, $\varepsilon_1$, $\varepsilon_2$ and $M$. As in the proof of Lemma~\ref{lem:fibres}, properness yields an open set $\mathcal V\ni F(q)$ with $F^{-1}(\mathcal V)\subset\mathcal N\cup\mathcal N_1\cup\dots\cup\mathcal N_n$. Let $Y_2$ be the set of points $w=G(q)+Ue+Ve'$ with $|U|<\varepsilon_1$, $|V|<\varepsilon_2$ and $(c,w)\in\mathcal V\cap F(\mathcal N_1)\cap\dots\cap F(\mathcal N_n)$. It is an open neighbourhood of $G(q)$. Let $w\in Y_2$. The fibre of $(c,w)$ consists of one point in each $\mathcal N_j$, at which $J>0$, and of the points of $F^{-1}(c,w)\cap\mathcal N$. If $V>M(U)$, there are two of the latter, one with $J<0$ and one with $J>0$ (Lemma~\ref{lem:foldnormal}(c)), so $n_+-n_-=(n+1)-1=n$. If $VA^*\},\qquad \mathcal I_U=F(\cD)\cap\{AA^*,\ w\in\mathrm{In}(R_c)\}$, $\mathcal I_U=\{(c,w):cA^*\}\subset\mathcal I_L$, which is connected. The same argument applies to $\mathcal I_U$. Now let $(c_1,w_1)$ and $(c_2,w_2)$ be points of $\mathcal O$ with $c_1\le c_2$. Then $w_1\ne0$ and $w_2\ne0$, since $(c,0)\in F(\Db)$ for all $c$ by Corollary~\ref{cor:slices}. By Corollary~\ref{cor:levels}, $B=\max\{|G(a)|:a\in\Db,\ c_1\le A(a)\le c_2\}$ is finite. Moreover $R_c\le B$ for $c\in[c_1,c_2]\setminus\{A^*\}$ because $C(R_c)=G(\Gamma_c)$. Fix $\lambda>\max(B,|w_1|,|w_2|)$, and put $\hat w_k=w_k/|w_k|$. Consider the path that runs from $(c_1,w_1)$ radially to $(c_1,\lambda\hat w_1)$, then at constant $G$ to $(c_2,\lambda\hat w_1)$, then along the circle of radius $\lambda$ to $(c_2,\lambda\hat w_2)$, and finally radially to $(c_2,w_2)$. The radial parts of the path lie in $\mathcal O$ by Lemma~\ref{lem:polar}(c), or since $w\ne0$ when $c=A^*$. The other two parts consist of points $(c,w)$ with $|w|=\lambda>B$. These lie in $\mathrm{Out}(R_c)$ for $c\ne A^*$, and they have $w\ne0$ for $c=A^*$. The whole path therefore lies in $\mathcal O$. \end{proof} \begin{theorem}\label{thm:degtwo} At every regular value $\mu$ of $F$, $n_+(\mu)-n_-(\mu)=2$. More precisely, $n_-=1$ and $n_+=3$ on $F(\cD)$, and $n_-=0$ and $n_+=2$ on $\R^3\setminus F(\Db)$. These two sets make up the regular values. \end{theorem} \begin{proof} Lemma~\ref{lem:locconst} shows that $n_+$ and $n_-$ are locally constant on the regular values. By Proposition~\ref{prop:components}, the regular values form the three open path-connected sets $\mathcal I_L$, $\mathcal I_U$ and $\mathcal O$, so $n_+$ and $n_-$ are constant on each of them. Let $d_L$, $d_U$ and $d_{\mathcal O}$ be the values of $n_+-n_-$ on these three sets. For $A_0$ large the point $(A_0,0,0)$ is a regular value with $n_-=1$ and $n_+=3$, by Proposition~\ref{prop:base}. Since the preimage of $(A_0,0,0)$ with $J<0$ lies in $\cD$ and $A_0>A^*$, the point lies in $\mathcal I_L$. Hence $d_L=2$. Fix $c>A^*$ and the fold point $q_c=\gamma_c(60^\circ)$. Lemma~\ref{lem:foldcross} yields a neighbourhood $Y_2$ of $G(q_c)$. As $G(q_c)\in C(R_c)$, there are points $w_{in}\in Y_2\cap\mathrm{In}(R_c)$ and $w_{out}\in Y_2\cap\mathrm{Out}(R_c)$ by Lemma~\ref{lem:polar}(d). By Proposition~\ref{prop:components}(b), $(c,w_{in})\in\mathcal I_L$ and $(c,w_{out})\in\mathcal O$. These two regular values have the same value of $n_+-n_-$ by Lemma~\ref{lem:foldcross}, so $d_{\mathcal O}=d_L$. The same argument with $c0$. Any $k$ distinct points of the fibre with $J>0$ persist, by the inverse function theorem, to $k$ distinct preimages with $J>0$ of any $\mu'$ near $\mu$. The point $\mu$ is a limit of points of $\mathcal O$. Indeed, if $\mu=(c,w)$ with $c\ne A^*$, then $w\in C(R_c)$ by Corollary~\ref{cor:slices}, and Lemma~\ref{lem:polar}(d) applies. Otherwise $\mu=F(p^*)$, the limit of the points $(A^*,w)\in\mathcal O$ as $w\to0$. As $n_+=2$ on $\mathcal O$, we get $k\le2$, so $1\le c_4(\mu)\le3$. Finally, the critical values form a closed set (proof of Lemma~\ref{lem:locconst}), and a null set by Sard's theorem \cite{Sar42}. This proves Proposition~\ref{prop:regcount}.\qed \section{The count at critical values}\label{sec:critical} In this section we compute $c_4(\mu)=\#F^{-1}(\mu)$, for $\mu\in\R^3$, at the critical values $\mu$ of $F=F_4$. Off the mirrors the points of $\Sigma\setminus\{p^*\}$ are fold points (Proposition~\ref{prop:classify}), the generic case in Whitney's theory of planar maps \cite{Whi55}. At fold points the count follows from the fold normal form and Theorem~\ref{thm:degtwo} (Section~\ref{sec:foldpoints}). But at the cusp points on the mirrors and at the umbilic the certified signs alone do not determine the local degree. There we will combine them with a normal form (Section~\ref{sec:cusppoints}) and with the closed form of the $2$-jet at $p^*$ (Section~\ref{sec:umbilic}). We keep the notation of Section~\ref{sec:thm1}. As a set, $\Sigma=\Sigma_L\sqcup\{p^*\}\sqcup\Sigma_U$. For $c\ne A^*$, $\Phi_c=A^{-1}(c)\cap\Db$ is a closed disk (Corollaries~\ref{cor:levels} and~\ref{cor:disk}), which lies in $\Db_L$ if $c>A^*$ and in $\Db_U$ if $c0$, we have $n_+-n_-=2$. \item $F$ is injective on $\Db$. \item $A>A^*$ on $\Db_L$ and $AA^*$ and $\Theta=\varphi+180^\circ$ if $c0$. \item Every point of $\Sigma\cap W$ other than $p^*$ lies in a leaf of type F or B of the core, lower core, top core or umbilic cover. At every point of $\Sigma\setminus\{p^*\}$, $T_1>0$ and $T_2<0$. At every point of $\Sigma\cap W$ in a leaf of type F, and at every point of $\Sigma\cap W$ off the mirrors in a leaf of type B, $T_3<0$. \end{enumerate} \end{lemma} \begin{proof} Part (a) is Theorem~\ref{thm:degtwo}, and (b) is Theorem~\ref{thm:inj}(a). Part (c) is Lemma~\ref{lem:levels}(a),(b) with Corollary~\ref{cor:levels}. For (d), the first statement is Proposition~\ref{prop:graph}, and the third is Theorem~\ref{thm:inj}(b). The second statement and the values of $\Theta$ at the mirrors are Proposition~\ref{prop:angle}: over the wedge $\Theta$ runs from $30^\circ$ to $90^\circ$ on the lower nappe and from $210^\circ$ to $270^\circ$ on the upper nappe. The axis meets $\Db_L$ in the segment $1/\sqrt3A^*$ it meets $\Phi_c$ in exactly one point $a_c$, which lies in $\Phi_c^\circ$. Because $P=Q=0$ on the axis, $G(a_c)=0$. The case $c0$ persist as preimages with $J>0$ of all nearby values, among them points of $\mathcal O$, where $n_+=2$. Part (f) follows from Lemma~\ref{lem:raysfacts}(d), Table~\ref{tab:types} and Lemma~\ref{lem:band}. Lemma~\ref{lem:foldsigns} extends its second statement to $\Om$. The leaves of types F and B occur only in the four covers listed (Table~\ref{tab:covers}). \end{proof} \begin{lemma}\label{lem:dA} $dA\ne0$ at every point of $\Om$. \end{lemma} \begin{proof} Where $J\ne0$, $dF$ is invertible and $dA\ne0$. At a point of $\Sigma\setminus\{p^*\}$, $T_2<0$ by Lemma~\ref{lem:facts}(f). The formula $T_2=\Av_s(\nabla\Jt)_r-\Av_r(\nabla\Jt)_s$ then shows that the vector $\Av=(-K)\nabla A$ is nonzero there. As $K<0$, it follows that $dA\ne0$. At $p^*$, $\partial_sA<0$ by Lemma~\ref{lem:axis}(c). \end{proof} \begin{lemma}\label{lem:images} \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item For $c\ne A^*$, $\Sigma\cap A^{-1}(c)=\Gamma_c$ and $F(\Db)\cap\{A=c\}=\{c\}\times(V_{in}(c)\cup C_c)$. \item $F(\Db)\cap\{A=A^*\}=\{F(p^*)\}=\{(A^*,0,0)\}$. \item If $\mu'\notin F(\Db)$, then $\mu'$ is a regular value of $F$ with exactly two preimages, at both of which $J>0$. This applies to $\mu'=(c,w)$ with $c\ne A^*$ and $w\in V_{out}(c)$, and to $\mu'=(A^*,w)$ with $w\ne0$. \end{enumerate} \end{lemma} \begin{proof} (a) We have $\Sigma\subset\Db$, $\Db\cap A^{-1}(c)=\Phi_c$ by Lemma~\ref{lem:facts}(c), and $\Phi_c\cap\Sigma=\Gamma_c$. Lemma~\ref{lem:facts}(d) shows that $G(\Phi_c)=V_{in}(c)\cup C_c$. (b) follows from Lemma~\ref{lem:facts}(c), because $P=Q=0$ on the axis. (c) A preimage with $J\le0$ would lie in $\Db$. Then $n_-(\mu')=0$, so $\#F^{-1}(\mu')=n_+(\mu')=2$ by Lemma~\ref{lem:facts}(a). \end{proof} \begin{lemma}[local count]\label{lem:localcount} Let $q\in\Sigma$ and $\mu=F(q)$. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $F^{-1}(\mu)=\{q\}\cup\{p_1,\dots,p_n\}$ with $n\le2$ and $J(p_j)>0$. In particular $c_4(\mu)=n+1$. \item Let $\mathcal N_0$ be an open neighbourhood of $q$ whose closure contains none of the $p_j$. There is a neighbourhood $\mathcal V$ of $\mu$ such that $\#F^{-1}(\mu')=n+\#(F^{-1}(\mu')\cap\mathcal N_0)$ for every $\mu'\in\mathcal V$. \item If some $\mu'\in\mathcal V\setminus F(\Db)$ has exactly $k$ preimages in $\mathcal N_0$, then $c_4(\mu)=3-k$. \end{enumerate} \end{lemma} \begin{proof} (a) By Lemma~\ref{lem:facts}(b), the points of $F^{-1}(\mu)$ other than $q$ lie outside $\Db$ and have $J>0$. There are at most two of them by Lemma~\ref{lem:facts}(e). (b) By the inverse function theorem there are pairwise disjoint open sets $\mathcal N_j\ni p_j$, disjoint from $\mathcal N_0$, such that $F$ maps each $\mathcal N_j$ diffeomorphically onto an open neighbourhood $\mathcal V_j$ of $\mu$. Let $B$ be a closed ball around $\mu$. As $F$ is proper (Proposition~\ref{prop:proper}), the set $F^{-1}(B)\setminus(\mathcal N_0\cup\mathcal N_1\cup\dots\cup\mathcal N_n)$ is compact; its image does not contain $\mu$. Let $\mathcal V\subset B\cap\mathcal V_1\cap\dots\cap\mathcal V_n$ be an open ball around $\mu$ that avoids this image. For $\mu'\in\mathcal V$ all preimages lie in $\mathcal N_0\cup\mathcal N_1\cup\dots\cup\mathcal N_n$, exactly one in each $\mathcal N_j$. (c) By (b) and Lemma~\ref{lem:images}(c), $n+k=2$. Then $c_4(\mu)=n+1=3-k$ by (a). \end{proof} The number $k$ is the local degree of $F$ at $q$. At cusp points and at $p^*$ we compute it with $\mu'=(A(q),w)$, where $w\in V_{out}(A(q))$ is close to $G(q)$, or $w\ne0$ is small if $q=p^*$. With $A$ as a coordinate near $q$ (Lemma~\ref{lem:dA}), the preimages of $\mu'$ near $q$ are the preimages of $w$ near $q$ under the planar map $g_c=G|_{\{A=c\}}$, where $c=A(q)$. At fold points the count follows from Lemma~\ref{lem:foldcross} and Theorem~\ref{thm:degtwo} instead. \subsection{Fold points}\label{sec:foldpoints} Recall from Section~\ref{sec:injective} that a point $q\in\Sigma\setminus\{p^*\}$ is a fold point if $T_3(q)\ne0$. \begin{lemma}\label{lem:foldkernel} At a fold point $q$, $\dim\ker dF(q)=1$, and $\ker dF(q)$ is transverse to $\Gamma_{A(q)}$. \end{lemma} \begin{proof} Put $c=A(q)$. Since $J(q)=0$ and $dA(q)\ne0$, the kernel $\ker dF(q)=\ker dA(q)\cap\ker dG(q)$ has dimension $1$ or $2$. By Lemma~\ref{lem:foldformulas}(c), the vector $v=\nabla A\times\nabla\Jt$ is tangent to $\Gamma_c$ at $q$. It is nonzero, since its $e_\varphi$-component is $T_2/(-K)\ne0$. If $\dim\ker dF(q)=2$, then $\ker dF(q)=\ker dA(q)\ni v$. If $\ker dF(q)$ is a line that is not transverse to $\Gamma_c$, it is spanned by $v$. In both cases $dG(q)v=0$, hence $d\Theta(v)=0$, since $G(q)\ne0$ by Lemma~\ref{lem:facts}(d). Then $T_3(q)=(P^2+Q^2)(-K)\,d\Theta(v)=0$ by Lemma~\ref{lem:foldformulas}(c), a contradiction. \end{proof} \begin{proposition}\label{prop:foldcount} If $q$ is a fold point, then $c_4(F(q))=3$. \end{proposition} \begin{proof} Put $c=A(q)$, and let $n$ be the number of points of $F^{-1}(F(q))$ other than $q$, so that $c_4(F(q))=n+1$. Lemma~\ref{lem:foldcross} provides an open neighbourhood $Y_2$ of $G(q)$ such that $n_+(c,w)-n_-(c,w)=n$ for each $w\in Y_2$ for which $(c,w)$ is a regular value. As $q\ne p^*$, we have $c\ne A^*$ and $G(q)\in C(R_c)$ (Theorem~\ref{thm:inj}). By Lemma~\ref{lem:polar}(d), $Y_2$ contains a point $w$ of $\mathrm{Out}(R_c)$. The point $(c,w)$ is a regular value by Proposition~\ref{prop:components}. Theorem~\ref{thm:degtwo} gives $n_+-n_-=2$ at $(c,w)$. Hence $n=2$ and $c_4(F(q))=3$. \end{proof} Lemma~\ref{lem:foldnormal} shows that the values $(c,w)$ near $F(q)$ with $V>M(U)$ have exactly two preimages near $q$, one with $J<0$ and one with $J>0$, while those with $V0$, the coordinates $(s,r,\varphi)$ are valid near $q$. In them the Jacobian determinant of $(A,L,\varphi)$ is $\partial_sA\,\partial_rL-\partial_rA\,\partial_sL=D_1$. At $q$ it equals $\Jm(q)/(-K(q))\ne0$, by $\Jm=\Av_s\partial_rL-\Av_r\partial_sL$ and $\Av=(-K)\nabla A$. The inverse function theorem shows that $(A,L,\varphi)$ are coordinates on a neighbourhood of $q$. We shrink it to a box centred at $q$ in these coordinates on which $D_1\ne0$. This box is $\sigma_m$-invariant. (c) As $A$ and $L$ are $\sigma_m$-invariant, $\sigma_m$ reads $(A,l,\varphi)\mapsto(A,l,2\varphi_m-\varphi)$ in these coordinates. From $L^\perp\circ\sigma_m=-L^\perp$, the function $h(A,l,\varphi)=L^\perp$ is odd in $\tau=\varphi-\varphi_m$. Hence $h=\tau H$ with $H(A,l,\tau)=\int_0^1\partial_\tau h(A,l,t\tau)\,dt$, where the box contains the segments of integration. This function is analytic and even in $\tau$. An analytic function that is even in $\tau$ is an analytic function of $\tau^2$, which defines $\widetilde H$. (d) The determinant of $\partial(A,L,L^\perp)/\partial(A,l,\varphi)$ is $\partial_\varphi h$. By the chain rule it equals $rJ/D_1$: the determinants of $\partial(A,L,L^\perp)/\partial(A,P,Q)$ (a rotation), $\partial(A,P,Q)/\partial(s,x,y)$, $\partial(s,x,y)/\partial(s,r,\varphi)$ and $\partial(s,r,\varphi)/\partial(A,l,\varphi)$ are $1$, $J$, $r$ and $1/D_1$. The last statement follows from Lemma~\ref{lem:images}(a). (e) At the points of the mirror, $\partial_\varphi A=\partial_\varphi L=0$. Since $D_1\ne0$, implicit differentiation gives $\partial s/\partial\varphi=\partial r/\partial\varphi=0$ at fixed $(A,l)$, that is, $\partial_\varphi|_{(A,l)}=\partial_\varphi|_{(s,r)}$ there. In particular $\widetilde H(0,0)=H(c,L(q),0)=\partial_\tau h(q)=\partial_\varphi L^\perp(q)=0$. Next, let $\omega$ denote the second argument of $\widetilde H$ and put $j(u,\tau):=\partial_\tau[\tau\widetilde H(u,\tau^2)]=\widetilde H(u,\tau^2)+2\tau^2\partial_\omega\widetilde H(u,\tau^2)$. By (d), $j=rJ/D_1$ on the level surface. Moreover $j(u,0)=\widetilde H(u,0)$. In particular $\hat a=\partial_uj(0,0)$. At fixed $(A,\varphi)$ the coordinate field is $\partial_l=(-\partial_rA\,\partial_s+\partial_sA\,\partial_r)/D_1$. At $q$, where $J=0$, we have $\nabla\Jt(q)=(-K)\nabla J(q)$ and $T_2(q)=K^2(\partial_sA\,\partial_rJ-\partial_rA\,\partial_sJ)(q)$. Then \[ \hat a=\frac{r}{D_1}\,\partial_lJ(q)=\frac{r}{D_1^2}\,\frac{T_2}{K^2}(q)=\frac{r\,T_2}{\Jm^2}(q), \] using $\Jm=(-K)D_1$. This is negative because $T_2(q)<0$ (Lemma~\ref{lem:facts}(f)). \end{proof} \begin{lemma}[the cusp is of order three]\label{lem:cuspthree} In the situation of Lemma~\ref{lem:cuspnormal}, $\hat b:=\partial_\omega\widetilde H(0,0)\ne0$, and in fact $\hat b\,L(q)<0$. \end{lemma} \begin{proof} We first expand along $\Gamma_c$. Put $\hat j(u,\omega)=\widetilde H(u,\omega)+2\omega\,\partial_\omega\widetilde H(u,\omega)$. Lemma~\ref{lem:cuspnormal}(d) shows that $\Gamma_c$ is $\{\hat j(u,\tau^2)=0\}$ near $q$. As $\partial_u\hat j(0,0)=\hat a\ne0$ and $\partial_\omega\hat j(0,0)=3\hat b$, the implicit function theorem gives an analytic function $\chi$ with $\chi(0)=0$ and $\chi'(0)=-3\hat b/\hat a$ such that $\Gamma_c=\{u=\chi(\tau^2)\}$ near $q$. This is the parametrization of $\Gamma_c$ by $\varphi$ (Lemma~\ref{lem:facts}(d)). Along it \[ U(\tau):=L-L(q)=\chi(\tau^2)=-\tfrac{3\hat b}{\hat a}\tau^2+O(\tau^4),\qquad V(\tau):=L^\perp=\tau\,\widetilde H(\chi(\tau^2),\tau^2)=-2\hat b\tau^3+O(\tau^5), \] since $\widetilde H(\chi(\omega),\omega)=\hat a\chi(\omega)+\hat b\omega+O(\omega^2)=-2\hat b\omega+O(\omega^2)$. From $G=L\,e_m+L^\perp e_m^\perp$ we get $\Theta-\Theta_m=\arctan\bigl(V/(L(q)+U)\bigr)$ near $q$, where $\Theta_m=\varphi_m$ if $L(q)>0$ and $\Theta_m=\varphi_m+180^\circ$ if $L(q)<0$. The function $\Theta(\tau)$ is analytic, and \begin{equation}\label{eq:cuspexp} \Theta(\tau)-\Theta_m=-\frac{2\hat b}{L(q)}\tau^3+O(\tau^5),\qquad \frac{d\Theta}{d\tau}=-\frac{6\hat b}{L(q)}\tau^2+O(\tau^4). \end{equation} Next we bound $d\Theta/d\tau$ from below. Let $\mathcal L$ be the finite set of leaves of type F or B of the four covers of Lemma~\ref{lem:facts}(f). As these are closed sets, there is $\epsilon>0$ such that each member of $\mathcal L$ that meets the ball $B_\epsilon(q)$ contains $q$. No leaf of type F contains $q$: $T_3(q)=0$ by Lemma~\ref{lem:cuspnormal}(a), whereas Lemma~\ref{lem:facts}(f) would imply $T_3(q)<0$. Lemma~\ref{lem:facts}(f) and the choice of $\epsilon$ show that each point $p\in\Sigma\cap W\cap B_\epsilon(q)$ lies in a leaf of type F or B that contains $q$, hence in a leaf of type B. The cell $C$ of this leaf contains $p$ and $q$. Hence the mirror angle of $C$ is $\varphi_m=\varphi(q)$. If $p=(s,r,\varphi_m+\tau)$ with $\tau\ne0$, then $T_3(p)\le\frac{\tau^2}2\beta_C\kappa_C(p)$ by \eqref{eq:bandkappa}. We shrink $\epsilon$ so that on $\overline{B_\epsilon(q)}$ the functions $r$, $P^2+Q^2$ and the $\kappa_C$ lie between positive constants and $|T_2|$ is bounded. Let $\beta<0$ be the largest of the finitely many $\beta_C$ of the leaves of type B that contain $q$, and $\kappa_0>0$ the smallest value on $\overline{B_\epsilon(q)}$ of the finitely many functions $\kappa_C$ of their charts. Then $T_3(p)\le\frac{\tau^2}2\beta\kappa_0$. At the points of $\Sigma$, $T_2<0$, and $T_3<0$ off the mirror (Lemma~\ref{lem:facts}(f)). Along $\Gamma_c$ on the side of $W$, Lemma~\ref{lem:foldformulas}(c) yields \[ \frac{d\Theta}{d\tau}=\frac{r\,T_3}{(P^2+Q^2)\,T_2}\ \ge\ C_0\tau^2,\qquad C_0=\frac{\min r\cdot|\beta|\cdot\kappa_0}{2\max(P^2+Q^2)\cdot\max|T_2|}>0 . \] Since the reflection $\sigma_m$ maps $\Gamma_c$ to itself, reverses $\tau$ and maps $\Theta$ to $2\varphi_m-\Theta$, the function $\Theta(\tau)-\Theta_m$ is odd. So $d\Theta/d\tau$ is even; hence the bound holds on both sides of the mirror. With \eqref{eq:cuspexp} this yields $-6\hat b/L(q)+O(\tau^2)\ge C_0>0$ for small $\tau\ne0$. Hence $\hat b\ne0$ and $\hat bL(q)<0$. \end{proof} As $\hat a<0$ and $\hat bL(q)<0$, the function $U=-\frac{3\hat b}{\hat a}\tau^2+O(\tau^4)$ along $\Gamma_c$ has the sign of $-L(q)$, or equivalently $|L|<|L(q)|$ on $\Gamma_c\setminus\{q\}$ near a cusp point: the cusp of $C_c$ at $G(q)$ points away from the origin. \begin{lemma}[one-variable lemma]\label{lem:onevar} Let $\delta>0$, $\hat a\ne0$ and $\hat b>0$, and let $\widetilde H$ be a $C^2$ function on $[-\delta,\delta]\times[0,\delta^2]$ with $\widetilde H(0,0)=0$, $\partial_u\widetilde H(0,0)=\hat a$ and $\partial_\omega\widetilde H(0,0)=\hat b$ such that, on the whole rectangle, \begin{itemize}[leftmargin=3.5em] \item[(H1)] $\partial_\omega\widetilde H\ge\hat b/2$, \item[(H2)] $3\,\partial_\omega\widetilde H+2\omega\,\partial_\omega^2\widetilde H>0$, \item[(H3)] $\partial_u\widetilde H(u,0)$ has the sign of $\hat a$ for $|u|\le\delta$. \end{itemize} For $|u|\le\delta$ and $|\tau|\le\delta$ put $f_u(\tau)=\tau\widetilde H(u,\tau^2)$. There is $\varepsilon\in(0,\delta]$ such that for every $u$ with $|u|\le\varepsilon$ the following hold. \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item $f_u(\delta)=-f_u(-\delta)\ge\hat b\delta^3/4$ and $f_u'(\pm\delta)>0$. \item If $\hat au\ge0$, then $f_u$ is strictly increasing on $[-\delta,\delta]$ and $f_u'>0$ except at $\tau=0$ when $u=0$. \item If $\hat au<0$, there is $\tau_+(u)\in(0,\delta)$ with $f_u'>0$ on $[-\delta,-\tau_+)\cup(\tau_+,\delta]$, $f_u'<0$ on $(-\tau_+,\tau_+)$ and $f_u'(\pm\tau_+)=0$, and $M(u):=f_u(-\tau_+(u))=-f_u(\tau_+(u))>0$. \item For $|V|<\hat b\delta^3/4$, the number of $\tau\in(-\delta,\delta)$ with $f_u(\tau)=V$ is $3$ if $\hat au<0$ and $|V|0$ because $f_u$ is odd and decreases strictly on $[-\tau_+,\tau_+]$. For (d), in case (c) the function $f_u$ maps $[-\delta,-\tau_+]$ increasingly onto $[f_u(-\delta),M]$, $[-\tau_+,\tau_+]$ decreasingly onto $[-M,M]$ and $[\tau_+,\delta]$ increasingly onto $[-M,f_u(\delta)]$, while $|V|<\hat b\delta^3/4\le f_u(\delta)$. In case (b) it maps $[-\delta,\delta]$ increasingly onto $[f_u(-\delta),f_u(\delta)]$. For (e), $\tau_+(u)$ is a simple zero of $f_u'$, since $f_u''(\tau_+)\ne0$, hence continuous by the implicit function theorem. Given $\eta\in(0,\delta)$, $f_0'\ge f_0'(\eta)>0$ on $[\eta,\delta]$. It follows by continuity that $\tau_+(u)<\eta$ for $|u|$ small. Finally $M(u)=\tau_+(u)\,|\widetilde H(u,\tau_+(u)^2)|\to0$. \end{proof} \begin{proposition}\label{prop:cuspcount} If $q$ is a cusp point, then $c_4(F(q))=2$. \end{proposition} \begin{proof} By equivariance we may assume $q\in W$. Let $c$, $\varphi_m$, $\hat a$, $\hat b$, $\widetilde H$, $u$ and $\tau$ be as in Lemmas~\ref{lem:cuspnormal} and~\ref{lem:cuspthree}. These lemmas show that $\hat a\ne0$ and $\hat b\ne0$. Replacing the target coordinate $L^\perp$ by $-L^\perp$ if necessary, which changes $\widetilde H$ into $-\widetilde H$ and $(\hat a,\hat b)$ into $(-\hat a,-\hat b)$, we may assume $\hat b>0$. Continuity yields $\delta>0$ such that (H1)--(H3) hold, the rectangle lies in the chart of Lemma~\ref{lem:cuspnormal}, and the corresponding closed set avoids the other points of $F^{-1}(F(q))$. Let $\varepsilon$ be given by Lemma~\ref{lem:onevar}, and put $\mathcal N=\{|u|<\varepsilon,\ |\tau|<\delta\}\subset A^{-1}(c)$ and $\mathcal N_0=\{|A-c|<\eta,\ (u,\tau)\in\mathcal N\}$ for a small $\eta>0$. In the target coordinates $(U,V)=(L-L(q),L^\perp)$, the preimages in $\mathcal N$ of a point $(U,V)$ with $|U|<\varepsilon$ are the points $(U,\tau)$ with $f_U(\tau)=V$. Let $Y_0=\{|U|<\varepsilon,\ |V|<\hat b\delta^3/4\}$ and \[ E_3=\{(U,V):\ |U|<\varepsilon,\ \hat aU<0,\ |V|0$ on $\mathcal N\setminus\overline{\mathcal N_{mid}}$. As $J=D_1\,\partial_\tau(\tau\widetilde H)/r$ with $D_1/r$ of constant sign, $J$ has one strict sign on $\mathcal N_{mid}$ and the opposite one on $\mathcal N\setminus\overline{\mathcal N_{mid}}$. Suppose that $J<0$ on $\mathcal N\setminus\overline{\mathcal N_{mid}}$. A point $(U,0)$ with $0<|U|<\varepsilon$ and $\hat aU<0$ lies in $E_3$. Two of its three preimages, those with $|\tau|>\tau_+(U)$, lie in $\mathcal N\setminus\overline{\mathcal N_{mid}}$. They are two distinct points of $\Db$ with the same image under $F$, which contradicts Lemma~\ref{lem:facts}(b). Hence $J<0$ on $\mathcal N_{mid}$, so the points of $\mathcal N_{mid}$ lie in $\Phi_c^\circ$. Lemmas~\ref{lem:onevar}(c) and~\ref{lem:facts}(d) then give $E_3=g_c(\mathcal N_{mid})\subset V_{in}(c)$. Since $G$ is injective on $\Gamma_c$ (Lemma~\ref{lem:facts}(d)), the compact set $G(\Gamma_c\setminus\mathcal N)$ does not contain $G(q)$. Let $Y\subset Y_0$ be an open box around $G(q)$ that avoids it. Then $C_c\cap Y=\mathcal C\cap Y$. A point $w\in Y\cap V_{out}(c)$ lies neither on $C_c$ nor in $V_{in}(c)\supset E_3$, so by the count above it has exactly one preimage in $\mathcal N$. Points $w\in Y\cap V_{out}(c)$ exist arbitrarily close to $G(q)$. For them $(c,w)\notin F(\Db)$ by Lemma~\ref{lem:images}(c). Lemma~\ref{lem:localcount}(c) with $k=1$ now shows that $c_4(F(q))=2$. \end{proof} The proof shows that near a cusp point the map $F$ is a Whitney cusp \cite{Whi55}. The points of $E_3$, inside $C_c$, have three preimages near $q$, one of them with $J<0$. The points of $V_{out}(c)$ near $G(q)$ have one, at which $J>0$. The local degree is $+1$. \subsection{The umbilic}\label{sec:umbilic} \begin{proposition}\label{prop:umbcount} $c_4(F(p^*))=1$. That is, for the masses $(1,1,1,m^*)$ the only concave CC with body $4$ inside, up to similarity, is the equilateral triangle with body $4$ at its centre. \end{proposition} \begin{proof} We put $c^*=c(s^*)$. Recall that $c^*\ne0$ by Proposition~\ref{prop:U}. We first restrict $G$ to the level of $p^*$. Since $\partial_sA(p^*)<0$, near $p^*$ the level set $A^{-1}(A^*)$ is the graph $s=s_A(z)$ of an analytic function $s_A$. Like $A$, the function $s_A$ is $\Sym$-invariant. The differential of $s_A$ at $0$, an invariant linear form on the irreducible representation on $(x,y)$, vanishes. Hence $|s_A(z)-s^*|\le C_s|z|^2$ for small $|z|$. For $g_*(z)=G(s_A(z),z)$, Lemma~\ref{lem:jet} and $\lambda(s^*)=0$ imply \[ g_*(z)=c^*\bar z^{\,2}+E_*(z),\qquad |E_*(z)|\le C_*|z|^3\qquad(|z|\le\delta_*). \] Here we use $|\lambda(s_A(z))z|\le\sup|\lambda'|\,C_s|z|^3$ and $|c(s_A(z))-c^*|\,|z|^2\le\sup|c'|\,C_s|z|^4$. We also need a bound on the derivative of $E_*$. For real-linear and real-multilinear maps on $\mathbb C$, $|\cdot|$ denotes the operator norm. The map $g_*$ is real-analytic, as $G$ and $s_A$ are. Shrinking $\delta_*$ if necessary, we may assume that $g_*$ is real-analytic on a neighbourhood of the closed disk $|z|\le\delta_*$. The Taylor polynomial of order $2$ of $E_*$ at $0$ is the only polynomial of degree at most $2$ that agrees with $E_*$ up to $o(|z|^2)$. As $E_*(z)=O(|z|^3)$, the zero polynomial has this property. It follows that $E_*$ and its first and second derivatives vanish at $0$. Since $c^*\bar z^2$ is quadratic in $(x,y)$, we have $D^3E_*=D^3g_*$. Taylor's formula with integral remainder, applied to $DE_*$, now gives \[ |DE_*(z)|\le C_*'|z|^2\qquad(|z|\le\delta_*), \] where $C_*'$ is half the maximum of $|D^3g_*|$ on the disk $|z|\le\delta_*$. In the coordinates $(A,x,y)$ near $p^*$ (Lemma~\ref{lem:dA}), $F$ reads $(A,x,y)\mapsto(A,\widetilde G(A,x,y))$ with $\widetilde G(A^*,\cdot)=g_*$. We fix $\rho_0\in(0,\delta_*]$ with $16C_*\rho_0\le|c^*|$ and $3C_*'\rho_0\le|c^*|$, and we fix $\eta>0$. We take both so small that the coordinates are defined on the closed box $\{|A-A^*|\le\eta,\ |z|\le\rho_0\}$ and that this box contains none of the points $p_j$ of Lemma~\ref{lem:localcount}(a). Let $\mathcal N_0$ be the open box $\{|A-A^*|<\eta,\ |z|<\rho_0\}$. The preimages in $\mathcal N_0$ of a point $\mu'=(A^*,w)$ are the points $(A^*,z)$ with $|z|<\rho_0$ and $g_*(z)=w$. We show that there are exactly two of them if $0<|w|<|c^*|\rho_0^2/4$. Let $0<|w|<|c^*|\rho_0^2/4$, let $\zeta_+$ be a square root of $w/c^*$, and put $\zeta_-=-\zeta_+$, $z_\pm=\bar\zeta_\pm$, $t=|\zeta_+|$. Then $|w|=|c^*|t^2$ and $00$ the principal square root $\sqrt v$ satisfies $\operatorname{Re}\sqrt v>0$ and $(\operatorname{Re}\sqrt v)^2-(\operatorname{Im}\sqrt v)^2=\operatorname{Re}v$. Hence $\operatorname{Re}\sqrt v\ge(\operatorname{Re}v)^{1/2}$ for $\operatorname{Re}v>0$; in particular $\operatorname{Re}\sqrt{1-u}>1/2$ for $|u|<1/8$. For $|u|,|u'|<1/8$ the denominators in \[ \sqrt{1-u\vphantom{\cramped{u'}}}-1=\frac{-u}{\sqrt{1-u\vphantom{\cramped{u'}}}+1},\qquad \sqrt{1-u\vphantom{\cramped{u'}}}-\sqrt{1-u'}=\frac{u'-u}{\sqrt{1-u\vphantom{\cramped{u'}}}+\sqrt{1-u'}} \] have real parts greater than $1$. Therefore all $u$, $u'$ with $|u|,|u'|<1/8$ satisfy $|\sqrt{1-u}-1|\le|u|$, $|\sqrt{1-u\vphantom{\cramped{u'}}}-\sqrt{1-u'}|\le|u-u'|$ and $|\sqrt{1-u}+1|>1$. A point $z\in B_\pm$ solves $g_*(z)=w$ if and only if $\bar z^2=(w-E_*(z))/c^*=\zeta_\pm^2(1-u(z))$, that is, if and only if $\bar z=\zeta_\pm\sqrt{1-u(z)}$ or $\bar z=-\zeta_\pm\sqrt{1-u(z)}$. The second case does not occur in $B_\pm$, since it gives $|z-z_\pm|=|\bar z-\zeta_\pm|=t\,|\sqrt{1-u(z)}+1|>t$. The solutions in $B_\pm$ are thus the fixed points of the map \[ f_\pm:B_\pm\to\mathbb C,\qquad f_\pm(z)=\overline{\zeta_\pm\sqrt{1-u(z)}} . \] The map $f_\pm$ sends $B_\pm$ into itself, because $|f_\pm(z)-z_\pm|=t\,|\sqrt{1-u(z)}-1|\le t\,|u(z)|\tfrac1{16}|c^*|\,|z|^2\ge C_*\rho_0|z|^2\ge C_*|z|^3\ge|E_*(z)| . \] If $|z|<2t$, then $|z-z_\pm|>t/2$ for both signs, and \[ |c^*\bar z^{\,2}-w|=|c^*|\,|z-z_+|\,|z-z_-|>\tfrac14|c^*|t^2\ge4C_*\rho_0t^2\ge8C_*t^3\ge C_*|z|^3\ge|E_*(z)| . \] In both cases $g_*(z)-w=(c^*\bar z^2-w)+E_*(z)\ne0$. We conclude that for $0<|w|<|c^*|\rho_0^2/4$ the equation $g_*(z)=w$ has exactly two solutions with $|z|<\rho_0$, one in $B_+$ and one in $B_-$. Let $\mathcal V$ be the neighbourhood of $F(p^*)$ given by Lemma~\ref{lem:localcount}(b). For $w\ne0$ small enough, the point $\mu'=(A^*,w)$ lies in $\mathcal V$ and has exactly two preimages in $\mathcal N_0$. Moreover $\mu'\notin F(\Db)$ by Lemma~\ref{lem:images}(b),(c). Lemma~\ref{lem:localcount}(c), applied with $q=p^*$ and $k=2$, shows that $c_4(F(p^*))=1$. By Proposition~\ref{prop:ax}, $F(p^*)=\mu^{(4)}(1,1,1,m^*)$, and $p^*$ is the equilateral configuration with body $4$ at its centre. \end{proof} The local degree of $F$ at $p^*$ is $+2$. All values inside $C_c$ for $c$ near $A^*$ have four preimages near $p^*$, which is the coalescence of four solutions into one observed in \cite{RS16}. \subsection{Classification of the fold and location of the cusps}\label{sec:classify} \begin{lemma}\label{lem:iota} The map $\Sigma_L\to(A^*,\infty)\times S^1$, $q\mapsto(A(q),\Theta(G(q)))$, is a homeomorphism, and so is the map $\Sigma_U\to(-\infty,A^*)\times S^1$ defined in the same way. We write $\iota_L$ and $\iota_U$ for their inverses, and $\iota(A,\Theta)$ for $\iota_L(A,\Theta)$ or $\iota_U(A,\Theta)$ according as $A>A^*$ or $AA^*$ (Lemma~\ref{lem:facts}(c)), and $\Theta\circ G$ maps each $\Gamma_c$ bijectively onto $S^1$ (Lemma~\ref{lem:facts}(d)). Since $G\ne0$ on $\Sigma_L$ (Lemma~\ref{lem:facts}(d)), the map is continuous. It is also proper: the preimage of $[\alpha,\beta]\times S^1$ is $\Sigma\cap\Db_L\cap A^{-1}[\alpha,\beta]$, a closed subset of a compact set (Lemma~\ref{lem:facts}(c)). A proper continuous map into a locally compact Hausdorff space is closed. A closed continuous bijection is a homeomorphism. The same holds for $\Sigma_U$. \end{proof} \begin{proposition}\label{prop:classify} \begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em] \item Every point $q\in\Sigma\setminus\{p^*\}$ is either a fold point or a cusp point, and not both. Points off the mirrors are fold points. At a mirror point exactly one of $\Jm(q)$ and $\partial_\varphi L^\perp(q)$ vanishes. A mirror point $q\in W$ is a cusp point if and only if it lies in a leaf of type B, if and only if $\partial_\varphi L^\perp(q)=0$. It is a fold point if and only if it lies in a leaf of type F, if and only if $\Jm(q)=0$. \item For each nappe and each of the six half-mirrors, the mirror points of that nappe on that half-mirror form a connected set, and they are either all fold points or all cusp points. \item The cusp points are the mirror points of $\Sigma_L$ on the half-mirrors $\varphi\in\{90^\circ,210^\circ,330^\circ\}$ and the mirror points of $\Sigma_U$ on the half-mirrors $\varphi\in\{30^\circ,150^\circ,270^\circ\}$. At all mirror points of $\Sigma_L$, $\Theta=\varphi$, and at all mirror points of $\Sigma_U$, $\Theta=\varphi+180^\circ$. In particular, for every $c\ne A^*$, $\Gamma_c$ has exactly three cusp points, those where $\Theta\circ G\in\{90^\circ,210^\circ,330^\circ\}$, and $C_c$ has a cusp at each of their images, pointing away from the origin. All other points of $\Gamma_c$, including the other three mirror points, are fold points. \end{enumerate} \end{proposition} \begin{proof} (a) Let $q\in W$, which lies in a leaf of type F or B by Lemma~\ref{lem:facts}(f). If $q$ is not on a mirror, then $T_3(q)<0$ in both cases: $q$ is a fold point and not a cusp point. If $q$ is a mirror point, then $0=\Jt(q)=(\partial_\varphi L^\perp(q)/r)\,\Jm(q)$ by Lemma~\ref{lem:mirror}. If $\Jm(q)\ne0$, then $q$ is a cusp point, $\partial_\varphi L^\perp(q)=0$ and $T_3(q)=0$ (Lemma~\ref{lem:cuspnormal}(a)). It is not a fold point. It lies in no leaf of type F, hence in a leaf of type B. If $\Jm(q)=0$, then $q$ lies in no leaf of type B, since the band certificate ensures $\Jm\ne0$ on the mirror face of the cell. The leaf of $q$ is then of type F, where $T_3(q)<0$ by Table~\ref{tab:types}. Then $T_3=L\,(\partial_\varphi L^\perp/r)\,T_2$ implies $\partial_\varphi L^\perp(q)\ne0$, so $q$ is a fold point and not a cusp point. Part (a) holds on $\Om$ by invariance. (b) By Lemma~\ref{lem:facts}(d), each circle $\Gamma_c$ meets each half-mirror $\varphi=\varphi_0$ in exactly one point, at which $\Theta=\varphi_0$ if $c>A^*$ and $\Theta=\varphi_0+180^\circ$ if $cA^*\}$, those of $\Sigma_U$ the connected set $\{\iota_U(c,\varphi_0+180^\circ):c\pi/2$, the zero has $s0$, that is, for $sR(A,\Theta)\}, \] and every point of $C_A$ is a boundary point of both $V_{in}(A)$ and $V_{out}(A)$. \item The sets $\Sigma_L\cup\{p^*\}$ and $\Sigma_U\cup\{p^*\}$ are homeomorphic to the open cone over a circle, with vertex $p^*$. Hence $\Sigma$ is homeomorphic to a double cone with vertex $p^*$. \end{enumerate} \end{lemma} \begin{proof} (a) This is Lemma~\ref{lem:levels}(c), since $\Sigma\subset\Db$. (b) Let $A\ne A^*$. By the definitions of $\iota$ and of $R_A$ (Proposition~\ref{prop:angle}), $R(A,\Theta)=R_A(\Theta)$. So $R(A,\cdot)$ is positive, and $C_A=C(R_A)$, $V_{in}(A)=\mathrm{In}(R_A)$ and $V_{out}(A)=\mathrm{Out}(R_A)$ are the three sets of the statement. Each point of $C_A$ is a boundary point of both $V_{in}(A)$ and $V_{out}(A)$ by Lemma~\ref{lem:polar}(d). Continuity off $A=A^*$ follows from Lemma~\ref{lem:iota}. If $(A_n,\Theta_n)\to(A^*,\Theta_0)$ with $A_n\ne A^*$, then $q_n=\iota(A_n,\Theta_n)$ satisfies $A(q_n)\to A^*$. Part (a) gives $q_n\to p^*$, so $R(A_n,\Theta_n)=|G(q_n)|\to|G(p^*)|=0$. For the invariance, let $g\in\Sym$. Then $F\circ g=\hat g\circ F$ with $\hat g(A,G)=(A,O_gG)$, and $g$ preserves $\Sigma_L$, $\Sigma_U$ and $A$. Therefore $O_gC_A=C_A$. As $O_g$ preserves lengths and acts on angles through $D_3$, $R(A,\cdot)$ is $D_3$-invariant. (c) By Lemma~\ref{lem:iota}, the map $q\mapsto(A(q),\Theta(G(q)))$, extended by sending $p^*$ to the vertex, is a bijection of $\Sigma_L\cup\{p^*\}$ onto the cone $([A^*,\infty)\times S^1)/(\{A^*\}\times S^1)$. It is continuous at $p^*$ because $A$ is continuous; its inverse is continuous at the vertex by (a). Elsewhere we use Lemma~\ref{lem:iota}. The same holds for $\Sigma_U\cup\{p^*\}$. These two sets are the closed subsets $\Sigma\cap\{s\le s^*\}$ and $\Sigma\cap\{s\ge s^*\}$ of $\Sigma$ (recall $\Sigma\subset\Db$). Since they meet only at $p^*$, their union $\Sigma$ is a double cone. \end{proof} Near $p^*$ the double cone is also the smooth picture. By Proposition~\ref{prop:U}, $J(p^*)=0$, $\nabla J(p^*)=0$ and $\operatorname{Hess}J(p^*)$ has signature $(-,+,+)$. By the Morse lemma, $\Sigma$ is then a quadratic cone at $p^*$ up to a diffeomorphism. In particular $\Sigma$ is not a $2$-manifold at $p^*$. \subsection{Certified points of the fold}\label{sec:certR} \begin{lemma}[certified points of the fold determine $R$]\label{lem:certR} Let $c\ne A^*$ and $\Theta_0\in S^1$. If $q\in\Om$ satisfies $J(q)=0$, $A(q)=c$ and $G(q)\in(0,\infty)\cdot e^{i\Theta_0}$, then $q=\iota(c,\Theta_0)$ and $R(c,\Theta_0)=|G(q)|$. Consequently, let $X$ be a box on which physicality is certified, and let $S$ be a set of parameters $(c,\Theta_0)$ with $c\ne A^*$. If for each $(c,\Theta_0)\in S$ the box $X$ contains a point $q$ with $\Jt(q)=0$, $A(q)=c$ and $G(q)\in(0,\infty)\cdot e^{i\Theta_0}$, then $R(c,\Theta_0)\in|G|(X)$ for all $(c,\Theta_0)\in S$. Such a point is, for instance, a zero of $(\Jt,\,A-c,\,\Theta\circ G-\Theta_0)$ or, at a mirror angle $\Theta_0$, a zero of $(\Jt,\,A-c)$ on the mirror plane at which $L$ has the sign that selects the ray. \end{lemma} \begin{proof} We have $q\in\Sigma\cap A^{-1}(c)=\Gamma_c$ by Lemma~\ref{lem:images}(a), and $\Theta(G(q))=\Theta_0$. The injectivity in Lemma~\ref{lem:iota} implies $q=\iota(c,\Theta_0)$, so $R(c,\Theta_0)=|G(q)|$ by definition. On a box where physicality is certified, $K<0$ and $\Jt=(-K)J$ vanishes exactly where $J$ does (Lemma~\ref{lem:foldformulas}(a)). \end{proof} In other words, an interval enclosure of a physical zero of either system is an enclosure of the point $\iota(c,\Theta_0)$ itself, so no search for other zeros is needed. \begin{remark}[effectivity]\label{rem:effective} Off the surface of critical values, $c_i(m)$ is decided by the sign of $\rho-R(A,\Theta)$ (Theorem~\ref{thm:count}), and by Lemma~\ref{lem:certR} an enclosure of $R(A,\Theta)$ can be obtained from an interval Newton or Krawczyk enclosure of one physical zero. Two systems are needed. \begin{itemize}[leftmargin=2em] \item For $\Theta$ off the six mirror rays, the point $q=\iota(A,\Theta)$ is not a mirror point, hence a fold point. The system $(\Jt,\,A-c,\,\Theta\circ G-\Theta)$ in $(s,x,y)$ has Jacobian determinant $\det[\nabla\Jt;\nabla A;\nabla\Theta]=-T_3/((P^2+Q^2)(-K))\ne0$ at $q$. \item For $\Theta$ on a mirror ray, $q$ is a mirror point. On the cusp rays $\Theta\in\{90^\circ,210^\circ,330^\circ\}$ we have $T_3(q)=0$, and the first system degenerates. On every mirror ray we use instead the system $(\Jt,\,A-c)$ on the mirror plane, where $G$ lies on the mirror line. In the coordinates $(s,r)$ of the plane its Jacobian determinant is $\partial_s\Jt\,\partial_rA-\partial_r\Jt\,\partial_sA=-T_2/(-K)\ne0$ at $q$. The sign of $L(q)$ decides which of the two opposite mirror rays is reached. \end{itemize} Near a regular zero the Krawczyk test succeeds on small boxes centred near it, at sufficient precision: with centred forms, the enclosures over a box converge as the box shrinks and the precision grows, so that the Krawczyk operator maps the box into its interior (see \cite[\S2.3 and Ch.~5]{Neu90}). These enclosures rest on the Krawczyk step for the implicit angles, which succeeds on small boxes since $\Lambda>0$ at physical points (Section~\ref{sec:balls}), and on jets of $K$ and $\mu$ up to order two, which $\nabla\Jt$ involves. As $|G(\iota(A,\Theta))|=R(A,\Theta)>0$, the angle $\Theta\circ G$ is defined near $\iota(A,\Theta)$. Since $\rho\ne R(A,\Theta)$ off the critical surfaces, four enclosures of values of $R$ at sufficient precision decide $N(m)$ for any $m$ outside $Z_1\cup\dots\cup Z_4$ whose masses are given exactly (for instance as rational or algebraic numbers). If $\rho=0$ no solve is needed: then $\rho0$ and $A=A^*$ (an algebraic condition on $m$, which rational masses never satisfy, since $m^{*3}$ is irrational), then $\rho>R(A,\Theta)=0$. If $\rho>0$ and $A\ne A^*$, a starting box comes from a floating-point solve (Section~\ref{sec:decide}) or, in principle, from an enumeration. Going through all pairs of a box with rational corners and a precision, one reaches a box on which the Krawczyk test succeeds and on which physicality and, for $\Theta$ on a mirror ray, the sign of $L$ that selects the ray are certified, since all of this holds, at sufficient precision, on small boxes centred near the regular zero $\iota(A,\Theta)$. By Lemma~\ref{lem:certR} every such box encloses $\iota(A,\Theta)$. \end{remark} \subsection{Proof of Theorem~\ref{thm:count}}\label{sec:proofcount} Let $R$ be the function of Lemma~\ref{lem:R}. It has the properties stated in Theorem~\ref{thm:count} by Lemma~\ref{lem:R}(b). Consider first $i=4$, and let $(A,\rho,\Theta)$ be the coordinates of $\mu=\mu^{(4)}(m)$. \begin{itemize}[leftmargin=2em] \item If $\rho0$. Thus $\mu$ is a regular value with $n_-=1$ and, by Lemma~\ref{lem:facts}(a), $n_+=3$, so $c_4=4$. \item If $\rho>R(A,\Theta)$ (this includes the case $A=A^*$, $\rho>0$), then $c_4=2$ by Lemmas~\ref{lem:R}(b) and~\ref{lem:images}(c). \item If $\rho=R(A,\Theta)$ and $A\ne A^*$, then $\mu=F(q)$ with $q=\iota(A,\Theta)\in\Gamma_A\subset\Sigma\setminus\{p^*\}$. By Proposition~\ref{prop:classify}, $q$ is a cusp point if $\Theta\in\{90^\circ,210^\circ,330^\circ\}$ and a fold point otherwise. Then $c_4=2$ and $c_4=3$, respectively, by Propositions~\ref{prop:cuspcount} and~\ref{prop:foldcount}. \item If $A=A^*$ and $\rho=0$, then $\mu=F(p^*)$ and $c_4=1$ by Proposition~\ref{prop:umbcount}. \end{itemize} The points with $\rho=R(A,\Theta)$ form $F(\Sigma)$, the set of critical values. For another body $i$, the map $F_i$ is $F_4$ after the labels $i$ and $4$ are exchanged. Then $c_i(m)=c_4(m')$, where $m'$ is $m$ with $m_i$ and $m_4$ exchanged. Also $\mu^{(4)}(m')=\mu^{(i)}(m)$ for the order of the outer bodies induced by the exchange. Another order replaces $(A,G)$ by $(A,O_gG)$ for some $g\in\Sym$. This leaves $A$ and $\rho$ unchanged and acts on $\Theta$ through $D_3$, which preserves $R$ (Lemma~\ref{lem:R}(b)) and the set $\{90^\circ,210^\circ,330^\circ\}$. This proves Theorem~\ref{thm:count}.\qed \subsection{Proof of Theorem~\ref{thm:N}}\label{sec:proofN} Section~\ref{sec:ccs} and \cite[\S2.2]{HM06} show that a non-collinear CC is convex or concave with exactly one body inside the triangle of the other three. We count each type in classes up to rotation, translation and scaling. Mirror images are counted separately. \begin{itemize}[leftmargin=2em] \item Collinear: exactly $4!/2=12$ \cite{Mou10}. \item Convex: for each of the $3$ cyclic orders, up to reversal, exactly one class up to similarity, by \cite{MB32,Xia04} for existence and \cite{Tom26} for uniqueness. In total $3\cdot2=6$. \item Concave with body $i$ inside: $2c_i$. \end{itemize} Adding, $N=12+6+2(c_1+c_2+c_3+c_4)$. Since the map $m\mapsto\mu^{(i)}(m)$ is a linear surjection onto $\R^3$ in the coordinates $\log m_1,\dots,\log m_4$, each set $Z_i$, the preimage of the set of critical values of $F_i$, is closed and null by Proposition~\ref{prop:regcount}. For the examples of item (d) we use the following lemma, which locates critical values on segments of masses. \begin{lemma}[crossing lemma]\label{lem:crossing} Let $m:[0,1]\to(0,\infty)^4$ be continuous, and let $X$ be a nonempty set of bodies whose mass coordinates $(A(t),\rho(t),\Theta(t))$ at $m(t)$ are the same for all $i\in X$ and all $t$, for suitable orders of their outer bodies. This holds, for instance, if $|X|=1$, or if the bodies of $X$ have the same mass and the same multiset of outer masses. Suppose that the following hold. \begin{enumerate}[label=\textup{(\arabic*)},leftmargin=2em] \item $\rho(t)>0$, $A(t)\ne A^*$ and $\Theta(t)\notin\{90^\circ,210^\circ,330^\circ\}$ for all $t\in[0,1]$. \item $\rho(0)R(A(1),\Theta(1))$, or the reverse. \item For every body $j\notin X$, $c_j(m(t))$ does not depend on $t$. This holds if $\rho^{(j)}-R(A^{(j)},\Theta^{(j)})$ has a constant strict sign on $[0,1]$, where $(A^{(j)},\rho^{(j)},\Theta^{(j)})$ are the mass coordinates of body $j$, or if $\rho^{(j)}\equiv0$ and $A^{(j)}(t)\ne A^*$ for all $t$. \end{enumerate} Then there is $t^*\in(0,1)$ with $c_i(m(t^*))=3$ for all $i\in X$, and $N(m(t^*))=\frac12\bigl(N(m(0))+N(m(1))\bigr)$. \end{lemma} \begin{proof} As $\rho>0$, the angle $\Theta(t)$ is continuous; hence $h(t)=\rho(t)-R(A(t),\Theta(t))$ is continuous by Lemma~\ref{lem:R}(b). It changes sign between $0$ and $1$ and vanishes at some $t^*\in(0,1)$. There $\rho=R(A,\Theta)$ with $A\ne A^*$ and $\Theta$ off the cusp rays: by the fourth row of Table~\ref{tab:count}, $c_i(m(t^*))=3$ for $i\in X$. The two sufficient conditions in (3) follow from the first two rows, and from the first row with $\rho=00$ and $\Theta=90^\circ$. Proposition~\ref{prop:palmore} shows that $\rho>R(-A^*/3,90^\circ)$, so Theorem~\ref{thm:count} gives $c_1=2$. Then $N(1,1,1,m^*)=18+2(1+2+2+2)=32$. Item (e) yields the same value without Proposition~\ref{prop:palmore} (Corollary~\ref{cor:rs}). (c) By Table~\ref{tab:count}, $c_i=2+2[\text{row }1]+[\text{row }4]-[\text{row }5]$, where $[\cdot]$ is $1$ if the mass coordinates of body $i$ lie in the given row and $0$ otherwise. Summing over $i$ gives $N=18+2(8+2k+f-p)=34+4k+2f-2p$; by the proof of (a), $p\le1$. Outside $Z_1\cup\dots\cup Z_4$, where no mass coordinates lie in rows $3$--$5$, $f=p=0$. (d) This is proved in Section~\ref{sec:examples} (Proposition~\ref{prop:examples}). (e) This is Corollary~\ref{cor:rs}. (f) The nullity of a CC does not change under similarities (including reflections), under relabellings of the bodies or under scalings of the masses. Indeed, between CCs normalized by $\lambda'=1$ a similarity is an isometry. These operations compose $V_m$ with an affine isometry of $(\R^2)^4$ or multiply it by a positive constant, which preserves the dimension of the kernel of its Hessian at corresponding critical points. Hence, by Lemma~\ref{lem:degen}, a concave CC with body $4$ inside and spokes $a$ has nullity $\dim\ker dF(a)$. It is degenerate exactly when $J(a)=0$. At a fold point $\dim\ker dF=1$ by Lemma~\ref{lem:foldkernel}. At a cusp point $q$, in the coordinates $(A,l,\varphi)$ of Lemma~\ref{lem:cuspnormal}, the first two components of $F$ have independent differentials that vanish on $\partial_\varphi$, and the derivative of the third along $\partial_\varphi$ is $\partial_\tau(\tau\widetilde H)(0,0)=\widetilde H(0,0)=0$. It follows that $\ker dF(q)$ is the line spanned by $\partial_\varphi$. Each point of $\Sigma\setminus\{p^*\}$ is a fold point or a cusp point (Proposition~\ref{prop:classify}(a)), and $\dim\ker dF(p^*)=2$ by Lemma~\ref{lem:axis}(d) and Proposition~\ref{prop:ax}. Proposition~\ref{prop:ax} identifies $p^*$ with the configuration named in (f). The configurations of $\Sigma$ form the degenerate concave CCs with body $4$ inside; $\Sigma$ is a double cone by Lemma~\ref{lem:R}(c). The other inner bodies follow by relabelling. (g) At equal masses the four points $\mu^{(i)}(1,1,1,1)=0$ have $A=0\ne A^*$ and $\rho=0R(A,\Theta)$, where $(A,\rho,\Theta)$ are its mass coordinates. Lemma~\ref{lem:certR} reduces this to the enclosure of one point of the fold. \subsection{The decision procedure}\label{sec:decide} For a body $i$ of an exactly given mass vector, a program computes ball enclosures of the mass coordinates from the exact masses and then proceeds as follows. All enclosures are computed in Arb ball arithmetic at $256$ bits, through \texttt{python-flint}, by an evaluator of the mass map independent of the C code of Section~\ref{sec:cert}. This evaluator encloses the implicit angles of Lemma~\ref{lem:angles} by a Krawczyk step valid for all spokes of a box. From them it computes the jets of $K$, $\mu$, $A$, $P$, $Q$ and $\Jt$, and from these the quantities $T_1$, $T_2$, $T_3$ and $\Jm$ of Section~\ref{sec:fold}. Physicality is certified on a box when all $a_i$ lie in $(0,1)$, the three angles lie in $(0,\pi)$ and $K<0$, by certified comparisons. Lemma~\ref{lem:angles} then shows that all points of the box are physical and carry the solution of that lemma. \begin{itemize}[leftmargin=2em] \item If the three outer masses are equal, then $\rho=0$ and the program certifies $A\ne A^*$. Then $\rho0$ for $\Theta=90^\circ$, $Q<0$ for $\Theta=270^\circ$), as Lemma~\ref{lem:certR} requires; the enclosure of $R$ is then $|Q|$. \item Otherwise $\Theta$ lies off the mirror rays. Let $(P_t,Q_t)$ be the target point in the $(P,Q)$-plane. The program uses the system $(\Jt,\,A-c,\,-Q_tP+P_tQ)$ in $(s,x,y)$ and certifies $P_tP+Q_tQ>0$ at the solution. The enclosure of $R$ is $(P_tP+Q_tQ)/|(P_t,Q_t)|$. \end{itemize} In both systems a Krawczyk test with centred forms, built from jets of order three at the centre and over the box, proves that the system has exactly one zero in a box on which physicality is certified. By Lemma~\ref{lem:certR} this zero is $\iota(A,\Theta)$, so its enclosure of $|G|$ is an enclosure of $R(A,\Theta)$. These are the two systems of Remark~\ref{rem:effective}, except that $-Q_tP+P_tQ$ replaces $\Theta\circ G-\Theta$. Where $P_tP+Q_tQ>0$, the two functions have the same zeros. The program then certifies a strict inequality between the enclosures of $\rho$ and of $R(A,\Theta)$, or, if it cannot, reports the body as undecided. Floating-point computations enter only to find starting points. For a segment of masses the program works with interval parameters. It covers the segment by subintervals on which the masses are balls containing $m(t)$ for all $t$ in the subinterval, encloses the mass coordinates over each subinterval, and solves the systems above with these balls as parameters. This enclosure of $R$ holds for all parameter values. A subinterval is decided if the enclosures of $\rho$ and of $R$ are strictly ordered. Undecided subintervals are bisected. \subsection{The examples}\label{sec:exlist} \begin{proposition}\label{prop:palmore} For the masses $(1,1,1,m^*)$, $c_1=c_2=c_3=2$. The mass coordinates of body $1$ are $A=-A^*/3$, $\rho=\frac{2}{\sqrt6}A^*=0.2128872401074461921835\ldots$ and $\Theta=90^\circ$, and \begin{gather*} R(-A^*/3,90^\circ)\in[0.011287144197733611\pm1.3\cdot10^{-19}],\\ \rho-R(-A^*/3,90^\circ)\in[0.2016000959097125813062817\pm2.9\cdot10^{-26}]. \end{gather*} \end{proposition} \begin{proof} Since the outer masses of body $1$ are $1$, $1$ and $m^*<1$, we have $P=0$, $\Theta=90^\circ$ and $A=\frac13\log m^*$. The program of Section~\ref{sec:decide} treats the masses $(m^*,1,1,1)$, which are $(1,1,1,m^*)$ after the labels $1$ and $4$ are exchanged. It encloses $m^*$ in a ball that contains $(81+64\sqrt3)/249$. For each of the three bodies of mass $1$ its mirror solve finds the point of the fold near $(s,x,y)=(0.74168,0,-0.00759)$, a cusp point on the half-mirror $\varphi=270^\circ$ of the upper nappe (Proposition~\ref{prop:classify}(c)). It returns an enclosure of $|Q|$ at this point and the stated enclosure of $\rho-R(-A^*/3,90^\circ)$. By Lemma~\ref{lem:certR}, the enclosure of $|Q|$ is one of $R(-A^*/3,90^\circ)$ itself. Hence $c_1=c_2=c_3=2$ by Theorem~\ref{thm:count}. Both enclosures are computed in ball arithmetic at $256$ bits, and the stated radii round up those of the program's log, which prints $R$ with $17$ significant digits and $\rho-R$ with $25$. \end{proof} \begin{proposition}\label{prop:examples} For the mass vectors and segments of Table~\ref{tab:examples}, the counts $c_i$ and $N$ are as stated. In particular every even value of $N$ from $32$ to $50$ is attained. \end{proposition} \begin{table}[ht] \centering\small \begin{tabular}{@{}r>{\raggedright\arraybackslash}p{2.75in}l>{\raggedright\arraybackslash}p{1.7in}@{}} \toprule $N$ & masses $(m_1,m_2,m_3,m_4)$ & $(c_1,c_2,c_3,c_4)$ & kind\\ \midrule $32$ & $(1,1,1,m^*)$ & $(2,2,2,1)$ & Palmore (Proposition~\ref{prop:palmore})\\ $34$ & $(1,2,3,4)$ & $(2,2,2,2)$ & regular\\ & $(1,51/50,26/25,53/50)$ & $(2,2,2,2)$ & regular\\ $36$ & $(1006,1000,994,500)$ $\to$ $(1007,1000,993,500)$ & $(2,2,2,3)$ & body $4$ crosses, $\Theta\approx60.1^\circ$\\ $38$ & $(1,1,1,1/2)$ & $(2,2,2,4)$ & regular\\ & $(1000,1001,1002,500)$ & $(2,2,2,4)$ & regular\\ $40$ & $(8000,8020,8041,8039)$ $\to$ $(8000,8020,8044,8036)$ & $(4,3,2,2)$ & body $2$ crosses, $\Theta$ from $207.5^\circ$ to $200.2^\circ$\\ & $(10000,10004,10038,10019)$ $\to$ $(10000,10004,10040,10020)$ & $(3,2,4,2)$ & body $1$ crosses, $\Theta\approx176.1^\circ$--$176.4^\circ$\\ $42$ & $(200,200,201,201)$ & $(4,4,2,2)$ & regular\\ & $(2000,2001,2010,2011)$ & $(4,4,2,2)$ & regular\\ $44$ & $(1,1,1,1001/1000)$ $\to$ $(1,1,1,1003/1000)$ & $(3,3,3,4)$ & bodies $1$, $2$, $3$ cross at $\Theta=270^\circ$\\ & $(10000,10004,10036,10018)$ $\to$ $(10000,10004,10038,10019)$ & $(4,3,4,2)$ & body $2$ crosses, $\Theta\approx180.03^\circ$\\ $46$ & $(2000,2000,2006,2003)$ & $(4,4,4,2)$ & regular\\ & $(125231/125000,$ $1002873/1000000,$ $24989/25000,1)$ & $(2,4,4,4)$ & regular\\ $48$ & $(10000,10000,10024,10012)$ $\to$ $(10000,10000,10028,10014)$ & $(4,4,4,3)$ & body $4$ crosses at $\Theta=270^\circ$\\ & $(10000,10001,10026,10013)$ $\to$ $(10000,10001,10028,10014)$ & $(4,4,4,3)$ & body $4$ crosses, $\Theta\approx268.1^\circ$\\ $50$ & $(1,1,1,1)$ & $(4,4,4,4)$ & regular\\ & $(10000,10001,10002,10004)$ & $(4,4,4,4)$ & regular\\ \bottomrule \end{tabular} \par\vspace{6pt} \caption{Certified examples. A regular example has all four statuses certified strictly. For a segment $m(t)=(1-t)m_a+tm_b$, $0\le t\le1$, the counts are those at a parameter $t^*\in(0,1)$ given by Lemma~\ref{lem:crossing}, and the angle is the value of $\Theta$ for the crossing body along the segment, with its outer bodies ordered as $j_10$; the tangential block is the Hessian of $U$ restricted to the sphere $\{I_m=I_m(x)\}$. The mixed terms vanish: $dV_m(tx)=t^{-2}dU(x)+\frac M2t\,dI_m(x)$ vanishes on $T_x\{I_m=I_m(x)\}$ for all $t$. Moeckel states that a Dziobek configuration is a nondegenerate critical point if and only if it has a smooth continuation to nearby masses and the map to mass space is a local diffeomorphism \cite[\S14]{Moe14}. He justifies this by the implicit function theorem, an argument that covers the direction from nondegeneracy to the local diffeomorphism. The following lemma gives a complete proof of both directions for concave configurations, through the transversality of the CC equations, and adds the identity between the nullity and $\dim\ker dF$. \begin{lemma}\label{lem:degen} Let $x$ be a concave CC with body $4$ inside, normalized by $\lambda'=1$, with spokes $a\in\Om$ and masses $m=(e^{F(a)},1)$. Then the nullity of $x$ equals $\dim\ker dF(a)$. In particular, $x$ is degenerate if and only if $J(a)=0$. \end{lemma} \begin{proof} We first pass to a slice. Let $\mathcal Y=\{x\in(\R^2)^4:\ x_4=0,\ x_1\in(0,\infty)\times\{0\}\}$, an open subset of a linear subspace of dimension $5$, which is transverse to the orbits of $SE(2)$ at the configurations with $x_1\ne x_4$ and meets each of them once. Each point of $\Om$ determines a configuration $y(a)\in\mathcal Y$ in which body~$2$ lies on the counterclockwise side of $x_1$, say. This map $a\mapsto y(a)$ is analytic and injective. It is an immersion, since the spokes are functions of $y$. Put $m'=(m_1,m_2,m_3)$ with $m_4=1$, and $\mathcal E(y,m')=\nabla(V_m|_{\mathcal Y})(y)\in\R^5$. Then $\mathcal E(y(a),m'(a))=0$ with $m'(a)=e^{F(a)}$ (Lemma~\ref{lem:dziobek}). As $\R^8=T_y\mathcal Y\oplus\mathfrak o_y$ and $V_m$ is invariant, the critical points of $V_m|_{\mathcal Y}$ are those of $V_m$, and $\ker\operatorname{Hess}V_m(y)=\ker\operatorname{Hess}(V_m|_{\mathcal Y})(y)\oplus\mathfrak o_y$. The nullity of $x$ is then $\dim\ker\mathcal H$, where $\mathcal H=\operatorname{Hess}(V_m|_{\mathcal Y})(y_0)$ and $y_0=y(a)$. Next we show that $D\mathcal E$ is onto. We have $D\mathcal E(y_0,m'_0)=[\mathcal H\mid\mathcal B]$ with $\mathcal Be_k=\nabla_yU_k$, where $U_k=\partial V_m/\partial m_k=\sum_{j\ne k}m_j\varphi_0(r_{kj})$. Let $\dot x\in T_{y_0}\mathcal Y$ be orthogonal to the image of $D\mathcal E$. Then $\mathcal H\dot x=0$, which puts $\dot x$ in $\ker\operatorname{Hess}V_m(y_0)$. Moreover $dU_k(\dot x)=0$ for $k=1,2,3$. Since $\sum_km_kU_k=2V_m$ and $dV_m(y_0)=0$, also $dU_4(\dot x)=0$. Write $Z_{kj}=(x_k-x_j)\cdot(\dot x_k-\dot x_j)$, a symmetric matrix with zero diagonal. Recall Dziobek's relations $m_km_jS_{kj}=\kappa\Delta_k\Delta_j$ from the proof of Lemma~\ref{lem:dziobek}, where $\kappa\ne0$ and $\Delta=(S_1,S_2,S_3,-S)$. They give \[ dU_k(\dot x)=-\sum_{j\ne k}m_jS_{kj}Z_{kj}=-\frac{\kappa\Delta_k}{m_k}(Z\Delta)_k, \] and since $\kappa\Delta_k/m_k\ne0$, we get $Z\Delta=0$. The linear map $Z\mapsto Z\Delta$ from symmetric matrices with zero diagonal to $\R^4$ has rank $4$. Indeed, with $f_k=e_k/\Delta_k$, the six elementary matrices have the images $\Delta_je_k+\Delta_ke_j=\Delta_j\Delta_k(f_k+f_j)$. They span $\R^4$ because the vectors $f_k+f_j$ do, the complete graph on four vertices not being bipartite. The kernel $\{Z:Z\Delta=0\}$ has dimension $6-4=2$. For a symmetric $2\times2$ matrix $M$, the infinitesimal deformation $\dot x_j=Mx_j$ has $Z_{kj}=(x_k-x_j)\cdot M(x_k-x_j)$ and $(Z\Delta)_k=\sum_j\Delta_jx_j\cdot Mx_j=:c_M$, independent of $k$ by $\sum_j\Delta_j=0$ and $\sum_j\Delta_jx_j=0$. The map $M\mapsto Z$ is injective: the six vectors $x_k-x_j$ of a configuration with no three bodies collinear have at least three pairwise independent directions, and a quadratic form on $\R^2$ that vanishes on three such directions is zero. Also $c_I=\sum_{i\le3}S_ia_i^2>0$ because $x_4=0$. Hence $\{M:c_M=0\}$ has dimension $2$, so its image is all of $\{Z:Z\Delta=0\}$. Each $\dot x$ with $Z\Delta=0$ is then of the form $\dot x=Mx+\zeta$ with $c_M=0$ and $Z(\zeta)=0$. Such a $\zeta$ is an infinitesimal isometry: the framework of the six segments on a configuration with no three bodies collinear is infinitesimally rigid in the plane, since the triangle $x_1x_2x_3$ is and $x_4$ is joined to it by three bars that are not all parallel. Now \[ \operatorname{Hess}V_m[\xi,\xi]=\sum_{i0$ and $\gamma^*<0$. Put $r_0=\nu^*/(2|\gamma^*|)$ and $w(\varphi)=2e^{i\varphi}-ie^{-2i\varphi}$. Then $f(r_0e^{i\varphi})=\kappa_s\,w(\varphi)$, and $w(\varphi)=e^{-i\pi/6}(2e^{it}+e^{-2it})$ for $t=\varphi+\pi/6$. So the image of the circle is the deltoid $\{2e^{it}+e^{-2it}:t\in\R\}$, scaled by $\kappa_s$ and turned through $-30^\circ$. Moreover \[ |w(\varphi)|^2=5-4\sin3\varphi,\qquad \operatorname{Im}\bigl(w'(\varphi)\,\overline{w(\varphi)}\bigr)=2+2\sin3\varphi . \] So $1\le|w|\le3$. The derivative $\operatorname{Im}(w'\bar w)/|w|^2$ of the argument of $w$ is positive except at three points. The argument increases by $360^\circ$ in total, since $|2e^{i\varphi}|>|e^{-2i\varphi}|$. It is therefore a homeomorphism of $S^1$. Thus the deltoid meets every ray from the origin once, and $R_{\mathrm d}$ is continuous. Where $\sin3\varphi=-1$ we have $w(\varphi)=3e^{i\varphi}$, and where $\sin3\varphi=1$ we have $w(\varphi)=e^{i\varphi}$. As $R_{\mathrm d}$ takes the value $\kappa_s|w(\varphi)|$ at the argument of $w(\varphi)$, this gives the extreme values of $R_{\mathrm d}$ and their positions. \emph{The level sets near $p^*$.} Put $\delta=A-A^*$. As $\partial_sA<0$ on the axis (Lemma~\ref{lem:axis}(c)), near $p^*$ the level set $\{A=A^*+\delta\}$ is the graph $s=s(A^*+\delta,z)$ of a function analytic in $(\delta,z)$. For $\zeta$ in a compact set and small $\delta\ne0$ put $\widehat G_\delta(\zeta)=\delta^{-2}G(s(A^*+\delta,\delta\zeta),\delta\zeta)$. As a function of $(\delta,\zeta)$ it extends real-analytically to $\delta=0$, where it equals $f(\zeta)$. Indeed, write $G=\lambda z+c\bar z^{\,2}+E$ as in Lemma~\ref{lem:jet}. First, $\lambda(s)$ is $s-s^*$ times an analytic function that equals $\lax'(s^*)$ at $s^*$. Second, $s(A^*+\delta,\delta\zeta)-s^*$ is $\delta$ times an analytic function of $(\delta,\zeta)$ that equals $1/\partial_sA(s^*)$ at $\delta=0$, since $\partial_xA=\partial_yA=0$ at $p^*$ (Lemma~\ref{lem:axis}(d)). Third, the Taylor coefficients of $E$ of order at most $2$ in $(x,y)$ vanish, since $|E|\le C_E|z|^3$. So $E$ is a sum of cubic monomials in $(x,y)$ with analytic coefficients; therefore $\delta^{-2}E(s(A^*+\delta,\delta\zeta),\delta\zeta)$ is $\delta$ times an analytic function. Hence $\widehat G_\delta(\zeta)-\nu^*\zeta-c(s^*)\bar\zeta^{\,2}$ is $\delta$ times an analytic function of $(\delta,\zeta)$, where $c(s^*)=i\gamma^*$ by Proposition~\ref{prop:U}. In particular $\widehat G_\delta\to f$ in $C^1$ on compact sets as $\delta\to0$. \emph{The fold curves near $p^*$.} By the chain rule and the proof of Lemma~\ref{lem:axis}(d), $J=\partial_sA\cdot\det D_zg_A(z)$ at the point $(s(A,z),z)$, where $g_A(z)=G(s(A,z),z)$ and $D_z$ is the derivative in $(x,y)$. As $g_A(\delta\zeta)=\delta^2\widehat G_\delta(\zeta)$, this determinant is $\delta^2j_\delta(\zeta)$, where $j_\delta$ is the Jacobian determinant of $\widehat G_\delta$. So $j_\delta(z/\delta)=0$ at the points $(s(A,z),z)$ of $\Gamma_A$ near $p^*$. \emph{The fold curves shrink at the rate $|\delta|$.} Lemma~\ref{lem:R}(a) shows that $\Gamma_A$ lies in any given neighbourhood of $p^*$ when $|\delta|$ is small. Near $p^*$ the proof of Proposition~\ref{prop:U} gives \[ J=\partial_sA\,\bigl(\lax'(s^*)^2(s-s^*)^2-4|c(s^*)|^2|z|^2\bigr)+O(\varrho^3),\qquad \varrho=\bigl((s-s^*)^2+|z|^2\bigr)^{1/2}. \] Since $J=0$ on $\Sigma$ and $\partial_sA\ne0$ near $p^*$, the bracket is $O(\varrho^3)$ on $\Sigma$. Let $C_1=|\lax'(s^*)|/|c(s^*)|$. At a point of $\Sigma$ with $|z|>C_1|s-s^*|$ the bracket is less than $-3|c(s^*)|^2|z|^2$ while $\varrho<(1+C_1^{-1})|z|$. This is impossible near $p^*$. So $|z|\le C_1|s-s^*|$ on $\Sigma$ near $p^*$. As $A-A^*=\partial_sA(s^*)\,(s-s^*)+O(\varrho^2)$, also $|s-s^*|\le C_2|\delta|$ on $\Gamma_A$ near $p^*$ for a constant $C_2$. Hence $|z|\le C|\delta|$ on $\Gamma_A$ for $C=C_1C_2$ and small $|\delta|$. \emph{Convergence of the fold curves.} The Jacobian determinant of $f$ is $j_0(\zeta)=|f_\zeta|^2-|f_{\bar\zeta}|^2=(\nu^*)^2-4(\gamma^*)^2|\zeta|^2$. As $(\nu^*)^2=4(\gamma^*)^2r_0^2$, we have $|j_0(\zeta)|\ge4(\gamma^*)^2r_0\,\bigl||\zeta|-r_0\bigr|$. Let $\epsilon_\delta$ be the maximum of $|j_\delta-j_0|$ on the disk $|\zeta|\le C$, divided by $4(\gamma^*)^2r_0$. Then $\epsilon_\delta\to0$, and $\bigl||\zeta|-r_0\bigr|\le\epsilon_\delta$ for $\zeta=z/\delta$ at every point $(s(A,z),z)$ of $\Gamma_A$. In particular $\zeta\ne0$ for small $|\delta|$. \emph{Convergence of the radius functions.} Let $C_f$ be a Lipschitz constant of $f$ on the disk $|\zeta|\le C+r_0$, and put $\eta_\delta=\max_{|\zeta|\le C}|\widehat G_\delta-f|+C_f\epsilon_\delta$. Then $\eta_\delta\to0$. Let $\Theta\in S^1$ and let $(s(A,z),z)$ be the point $\iota(A,\Theta)$ of $\Gamma_A$. Put $\zeta=z/\delta$. By the definition of $R$ (Lemma~\ref{lem:R}(b)), $\delta^{-2}R(A,\Theta)e^{i\Theta}=\delta^{-2}G(\iota(A,\Theta))=\widehat G_\delta(\zeta)$. This point lies within $\eta_\delta$ of the point $f(r_0\zeta/|\zeta|)$ of the deltoid, whose modulus is at least $\kappa_s$. So the arguments of the two points differ by at most $\arcsin(\eta_\delta/\kappa_s)$ once $\eta_\delta<\kappa_s$. Hence $|\delta^{-2}R(A,\Theta)-R_{\mathrm d}(\Theta)|$, the distance from $\delta^{-2}R(A,\Theta)e^{i\Theta}$ to $R_{\mathrm d}(\Theta)e^{i\Theta}$, is at most $\eta_\delta$ plus the oscillation of $\vartheta\mapsto R_{\mathrm d}(\vartheta)e^{i\vartheta}$ on intervals of length $\arcsin(\eta_\delta/\kappa_s)$. As this map is uniformly continuous, the bound tends to $0$, uniformly in $\Theta$. \end{proof} One question remains open: whether Theorem~\ref{thm:count} has a proof without computer assistance. The obstacle is that the fold has no closed form away from the axis: the sign of $J$ near it is known only box by box. In our proof the interval certificates supply the facts listed at the end of Section~\ref{sec:idea}. The closed forms of Section~\ref{sec:axis} replace them only on the axis and at the umbilic. \appendix \section{The corner and fin charts}\label{app:charts} In each of the charts $\mathrm{CH}_{110}$, $\mathrm{CH_{fin}}$ and $\mathrm{CH}_{111}$ the box coordinates $u$ and the implicit variables $v$ determine $a$ and a solution $(\theta,K)$ of $k_1=k_2=k_3=K$ with $\theta_3=2\pi-\theta_1-\theta_2$. The three equations $\Psi(u,v)=0$ are these equations divided by positive factors. Conversely, each physical point $a$ of the chart's region, defined below, determines a point $u(a)$ of the chart domain and a solution $v(a)$. With $d=\det\Psi_v$, implicit differentiation gives $d\,\partial\mu/\partial u=\mu_u\,d-\mu_v\operatorname{adj}(\Psi_v)\Psi_u$ and the same formula for $a$. We evaluate these with the rows of $\mu$ and of $a$ multiplied by positive factors or combined by row operations of determinant $1$, using logarithmic derivatives in the coordinates of $u$ that tend to $0$, none of which changes the signs of the two determinants. By the chain rule, $J=\det(\partial\mu/\partial u)/\det(\partial a/\partial u)$. We write $\mathfrak g(t)=(1+t+t^2)/t^3$, so that $t^{-3}-1=(1-t)\,\mathfrak g(t)$. \emph{Uniqueness.} For a box of $u$, we compute an a priori box $V^{\mathrm{big}}$ that contains $v(a)$ for all points $a$ of the region with $u(a)$ in the box, or prove that there is no such point. Uniqueness holds if each sub-box of an adaptive subdivision of the box either has an empty a priori box or satisfies $\|I-Y\Psi_v\|_\infty<1$ over the interval hull of its own a priori box and Krawczyk tube, with $Y$ the inverse of $\Psi_v$ at its centre. Then $\Psi(u,\cdot)$ has at most one zero in that hull, so that the zero of the Krawczyk step is the only point of the region over $u$. In $\mathrm{CH}_{110}$ and $\mathrm{CH}_{111}$, where $u$ is a function of $a$ alone, uniqueness also holds if the angles of the Krawczyk tube are principal, $0<\theta_1,\theta_2<\pi<\theta_1+\theta_2$, because by Lemma~\ref{lem:angles} the solution with principal angles is unique for each $a$. \emph{Types.} A leaf is of type P if the Krawczyk step succeeds over its box, $\det(d\,\partial\mu/\partial u)$ and $\det(d\,\partial a/\partial u)$ are of definite signs on the box with positive product, and uniqueness holds. Then $J>0$ at all physical points of the region over the box. A leaf is of type X if the a priori box is empty, or if uniqueness holds and the zero of the Krawczyk step lies outside the region throughout the box, by the tests listed below. Then no physical point of the region lies over the box. \emph{$\mathrm{CH_{fin}}$, the fin $a_1+a_2\to2$.} Here $u=(t,a_3,\theta_1)$ with $t=-K$. The implicit variables are $v=(\omega_1,\omega_2,\theta_2)$ with $w_i=t\,\omega_i$ for $i=1,2$, so that $a_i=(1+t\omega_i)^{-1/3}$. The equations are \[ \Psi=\bigl(\omega_1(q_1-1)+1,\ \omega_2(q_2-1)+1,\ w_3(q_3-1)+t\bigr), \] and $\mu_1=\log S_1+\log\omega_2+\log w_3-\log S$, $\mu_2=\log S_2+\log\omega_1+\log w_3-\log S$, $\mu_3=\log t+\log S_3+\log\omega_1+\log\omega_2-\log S$. We multiply the row of $\mu_1$ by $\sin\theta_1$ and divide the rows of $a_1$ and $a_2$ by $t$. The region is the set of physical $a$ with $a_1\ge a_2$, $a_1+a_2\ge\Tfin$ and $u(a)$ in the domain of the fin cover. We compute the a priori box from bounds valid on this region, as the exact check confirms. The tests for type X are $\omega_1>\omega_2$ (that is $a_1\pi$, and $a_1+a_2\pi$, $\theta_2>\pi$, and $\theta_1+\theta_2<\pi$ (that is $\theta_3>\pi$). \emph{$\mathrm{CH}_{111}$, the corner $a\to(1,1,1)$ and the fin tip.} Here $u=(\varsigma,\lambda,b)$ with $a_1=1-\varsigma\lambda b$, $a_2=1-\varsigma\lambda$ and $a_3=1-\varsigma$. The implicit variables are $v=(\kappa,\theta_1,\theta_2)$ with $K=-\varsigma\lambda\kappa$. The equations are \[ \Psi=\bigl(b\,\mathfrak g(a_1)(q_1-1)+\kappa,\ \mathfrak g(a_2)(q_2-1)+\kappa,\ \mathfrak g(a_3)(q_3-1)+\lambda\kappa\bigr), \] the equations $k_i=K$ divided by $\varsigma\lambda$, $\varsigma\lambda$ and $\varsigma$. The rows of $\mu$ are $\sin\theta_1\nabla(\mu_1-\mu_3)$, $\sin\theta_2\nabla(\mu_2-\mu_3)$ and $\kappa\nabla\mu_3$; the rows of $a$ are divided by $\varsigma\lambda b$, $\varsigma\lambda$ and $\varsigma$. The chart is regular at $\varsigma=0$, $\lambda=0$ and $b=0$. The region is the set of physical $a$ with $a_3\ge1-0.1$ and $a_1\ge a_2\ge a_3$. The tests for type X are those of $\mathrm{CH}_{110}$ with $\kappa$ in place of $\tau$. A leaf of type D is not evaluated. It is a box in $\hat r<0.184$, where $\hat r=|a-s(1,1,1)|/(1-s)$ is the coordinate of chart~$3$. The points of such a box routed to this cover in Section~\ref{sec:inclusion} have $1-s\le1/32$ and lie in the top covers. \section*{Data and code availability} The supplement to this paper on Zenodo (\href{https://doi.org/10.5281/zenodo.23256905}{doi:10.5281/\allowbreak zenodo.23256905}) contains the following parts. The README lists the SHA-256 hashes of the files of the first four parts, directly or through the hash lists of their directories. \begin{itemize}[leftmargin=2em] \item The C and Python sources of the certificates of Section~\ref{sec:cert}, the floating-point fold table of Section~\ref{sec:covers} and the logs of the run described in Section~\ref{sec:checklist}. The list \texttt{cert/\allowbreak runs/\allowbreak SHA256SUMS} contains the hashes of the $80$ files of that run, among them $12$ arrays that are not included: the $11$ covers and the array of pieces of the check of Proposition~\ref{prop:cert}(f). \item The programs and logs of the certified computations of Section~\ref{sec:examples} and of the separately written program of Section~\ref{sec:exlist} that re-certifies them. The script \texttt{exact/\allowbreak cert/\allowbreak run\_all.sh} regenerates the logs of the certified computations in about $20$ minutes, and \texttt{exact/\allowbreak judge/\allowbreak run\_judge.sh} reruns the re-certification. \item The exact computations behind the family theorem of Section~\ref{sec:family}. The script \texttt{analytic1/\allowbreak exact/\allowbreak run\_all.sh} reruns the polynomial and resultant computations. It reads the factor $\mathcal F$ of Section~\ref{sec:famcert} from the file \texttt{fold\_cache.pkl} if that file is present; after the file is deleted, it recomputes $\mathcal F$, with the same result. The program \texttt{exact/\allowbreak ref\_family/\allowbreak arc\_cert.py} is the certificate without resultants. It also certifies Proposition~\ref{prop:famcert}(a) and the signs in Proposition~\ref{prop:famcert}(c). \item The scripts \texttt{axis\_lambda.py}, \texttt{axis\_jet2.py} and \texttt{s3\_check.py} and their logs. These scripts check the closed forms of Propositions~\ref{prop:ax} and~\ref{prop:U} in exact arithmetic. The script \texttt{deg\_restricted.py}, its log and the module \texttt{fullmap.py}, which the script imports for one of its floating-point cross-checks. The script checks in exact arithmetic the identities of Section~\ref{sec:restricted} that the text cites by the labels of its checks. \item The sources of the Lean formalization, its certificate files, the programs that regenerate them and the SHA-256 hashes of these files. \end{itemize} A README maps the covers of Table~\ref{tab:covers} to their files and the labels of the bodies to those of the code. It also states the formulas of the region functions and the floating-point constants of the programs. The covers themselves (about $220$~MB) are not included, but the programs regenerate them deterministically. The script \texttt{cert/run\_checks.sh} regenerates them a second time, compares the two and runs all the checks of Section~\ref{sec:checklist}. In the regenerated covers the arrays of leaves equal those of the stored ones. The computations use FLINT/Arb~3.4.0 \cite{FLI25,Joh17} with gcc~15.2.0 for the C code, and CPython~3.14.4 with numpy~2.5.3, mpmath~1.3.0 \cite{mpm23}, \texttt{python-flint}~0.9.0 (with its own FLINT~3.6.0), SymPy~1.14.0, Singular~4.4.1 and msolve~0.9.4. For the floating-point cross-checks we also use SciPy~1.18.1. The computer-assisted part of the proof assumes the correctness of Arb, of the compiler, of the computer algebra systems and the Python libraries listed above, and of our own programs, whose sizes the README lists. The second evaluation of the leaves in Section~\ref{sec:checklist} calls the same compiled libraries as the programs that built the covers, so it detects errors in those programs and in the stored covers but not in the formulas that the libraries evaluate. A separately written program derives the type of each leaf of the fold-core, corner and fin covers from the reproduced enclosures. It recomputes the bounds of the band brackets in exact rational arithmetic. Two of the rigorous checks are independent of the compiled formulas: the leaves excluded by the $\alpha$-test are retested in mpmath, and all inclusions between regions are verified in exact rational arithmetic. The values computed by the C code are compared with a second rigorous implementation only in chart~$1$, at $100$ points. There the evaluator of Section~\ref{sec:examples} reproduces the values of $K$, $\hA$, $P$, $Q$, $\Jt$, $T_1$, $T_2$, $T_3$ and $\Jm$ computed by the C code (Section~\ref{sec:exlist}). The other quantities that the proof takes from the C code rest on this one implementation: the derivatives $\partial_rT_3$, $\partial_\varphi^2T_3$ and $\partial_\varphi^2\Jt$ of the band certificates (Section~\ref{sec:types}), the quantities of charts $0$, $2$, $3$ and $4$, among them those of the umbilic chart, and the quantities of the bulk, corner and fin charts. The floating-point checks of the covers described in the README compute $J$ independently of the compiled formulas, but only at sample points. The certified computations of Section~\ref{sec:examples} are re-certified by the separately written program of Section~\ref{sec:exlist}, which shares no code with the programs of Section~\ref{sec:examples} except the ball arithmetic. The Lean formalization does not depend on the correctness of any of these programs: in place of Proposition~\ref{prop:cert} it uses facts proved by hand or by certificates of its own, which use a different cover and certify different quantities. Some computations test the proof but are not part of it: the confirmation of the vanishing coefficients of Lemma~\ref{lem:jet} and of the value of $\gamma(s^*)$ in the proof of Proposition~\ref{prop:U}, the test of the vanishing coefficients at $p^*$ in Section~\ref{sec:balls}, the enclosure of $A$ at $s_{eq}(1,1,1)$ in the proof of Proposition~\ref{prop:cert}(g), the second proof of Lemma~\ref{lem:raysfacts}(b) by the covers, the enclosure of the axis point in Section~\ref{sec:decide}, the brackets of the crossing parameters, the comparisons of the evaluator of Section~\ref{sec:examples} with other programs, the independent re-certification in Section~\ref{sec:exlist}, the msolve and floating-point checks in Section~\ref{sec:famcert}, the floating-point counts in Section~\ref{sec:famcount}, the evaluation of the mass ratio at $s_a$ and $s_b$ and the numerical comparison with the deltoid in Section~\ref{sec:checks}, the floating-point checks of the covers described in the README, and three checks that \texttt{cert/\allowbreak run\_checks.sh} runs: the condition that $\partial_rK>0$ wherever $K=0$ on the leaves of types M, P, F and B in charts~$1$ and~$3$, lower bounds for $1-\zeta_i^2$ and for the Hessian of $g_\alpha$ on a box near the axis together with the location of the root boxes of the lower axis cover, and the largest $s$, $0.5927734375$, of a leaf of type M, F or B on which $K$ is not negative throughout. The formalization is written in Lean~4 \cite{dMU21}, version 4.35.0-rc3, with Mathlib \cite{mC20} at the corresponding tag. The main theorem of the formalization states Theorems~\ref{thm:count} and~\ref{thm:N} and takes no unproved inputs. For Theorem~\ref{thm:count} the formal statement contains the radius function $R$ with its properties, the five rows of Table~\ref{tab:count}, with $\Theta$ defined by one order of the outer bodies, and the description of the critical values for one inner body; for Theorem~\ref{thm:N} it contains the formula, in which $12$ counts the collinear and $6$ the convex CCs, and items (a)--(g). Besides definitions of Mathlib, these statements rest on $124$ definitions and one structure of the formalization. The README of the formalization lists the files that contain them and matches each part of the two statements with the paper. The main theorem depends only on the axioms \texttt{propext}, \texttt{Classical.\allowbreak choice} and \texttt{Quot.sound}, and no theorem in the $13{,}562$ modules of its import closure, Mathlib included, depends on another axiom. Beyond these axioms, the formal proof assumes the correctness of the Lean kernel, including its arithmetic of natural numbers. Two kernels implemented separately from Lean's, nanoda~0.4.17 and lean4lean, also accept every declaration on which the main theorem depends, read from an export of the compiled formalization (directory \texttt{kernel2} of the formalization). Outside the scratch and experiment directories, which nothing in the proof imports and which are not part of the supplement, the Lean files of the formalization contain no \texttt{sorry}, \texttt{native\_decide}, \texttt{implemented\_by} or \texttt{extern}. The cover of the formalization, with about $1.19$ million leaves, shares only the bounds of its regions with the paper, up to rounding. Most leaves enclose the solution of Lemma~\ref{lem:angles} by a Krawczyk test in half-angle tangents of the angles and the other quantities by Taylor models of order~$3$ with exact dyadic coefficients; the cones of the umbilic ball use first-order slopes along rays, and the remaining leaves exclude their boxes by algebraic tests. Instead of $\Jt$ and the other quantities of Section~\ref{sec:balls}, the leaves certify signs of the function $\det(I-M_{\mathrm C})$ of the remark below and of its derivatives. Further certificates take the place of the computations of Sections~\ref{sec:examples} and~\ref{sec:family} in the proof of Theorem~\ref{thm:N}; of Section~\ref{sec:examples} they certify only the counts of Proposition~\ref{prop:palmore} and one mass vector or segment of Table~\ref{tab:examples} for each value of $N$ from $34$ to $48$. In all, the kernel checks of the certificates take about $240$ CPU-hours, and some modules need up to about $27$~GB of memory. Regenerating the certificate files takes about $16$ CPU-hours. On the tested platform, CPython~3.14.4 on x86-64 Linux with glibc~2.43, the regenerated files are identical to the hashed ones. Elsewhere a regenerated file may differ, since its hints are rounded floating-point values that depend on the math library, and then the kernel check, not the hash, decides whether it is a valid certificate. Table~\ref{tab:formal} lists the items of Proposition~\ref{prop:cert} and the other ingredients of Sections~\ref{sec:thm1} and~\ref{sec:critical} that rest on the certificates of Section~\ref{sec:cert}, with their counterparts in the formal proof. \begin{table}[ht] \centering\small \begin{tabular}{@{}>{\raggedright\arraybackslash}p{1.5in}>{\raggedright\arraybackslash}p{3.2in}>{\raggedright\arraybackslash}p{1.1in}@{}} \toprule paper & formal proof & argument\\ \midrule Proposition~\ref{prop:cert}(a) & \texttt{sStar\_bounds}: $s_a\le s^*\le s_b$, from $s^{*3}=3/(6\sqrt3-2)$ & without a certificate\\\addlinespace[2pt] Proposition~\ref{prop:cert}(b): the covers of Table~\ref{tab:covers} & the cover \texttt{Final.\allowbreak coverHyp} with about $1.19$ million leaves (directories \texttt{CC50/\allowbreak Prod}, \texttt{CC50/\allowbreak Chart} and \texttt{CC50/\allowbreak Band2}), which certify signs of $\det(I-M_{\mathrm C})$ and its derivatives in place of $\Jt$, $T_1$, $T_2$ and $T_3$; \texttt{Agg.\allowbreak certFacts\_of\_cover} and \texttt{Agg.\allowbreak critCertFacts\_of\_cover} derive from it the certified facts that Sections~\ref{sec:thm1} and~\ref{sec:critical} use & the paper's\\\addlinespace[2pt] Proposition~\ref{prop:cert}(c) and the umbilic chart & a cover of the ball of radius $3/4000$ about $p^*$ in $W$ by $275$ cones, with slopes along the rays from $p^*$, where $M_{\mathrm C}=I$ (\texttt{Chart.\allowbreak UmbCov.\allowbreak umbBall\_cover}) & different\\\addlinespace[2pt] Proposition~\ref{prop:cert}(d) for leaves of types M, F and B, and (e) & the fields \texttt{resolved}, \texttt{top} and \texttt{star} of \texttt{Agg.\allowbreak DFacts}, which every leaf of types M, fold and band carries; \texttt{Agg.\allowbreak level\_star\_of\_cover} & the paper's\\\addlinespace[2pt] Proposition~\ref{prop:cert}(d) for leaves of type P, in the proof of Lemma~\ref{lem:raysfacts}(c) & none: the formal counterparts of Lemmas~\ref{lem:raysfacts}(c),(d) and~\ref{lem:rays}, \texttt{Agg.\allowbreak ray\_unique\_of\_cover} and \texttt{Agg.\allowbreak ray\_exists\_of\_cover}, need a resolved leaf only at non-physical limits of physical points with $J\le0$, and such a limit lies in a leaf of type M, fold or band & different\\\addlinespace[2pt] Proposition~\ref{prop:cert}(f) & the half-plane condition on each fold leaf (\texttt{Fold.\allowbreak foldLeaf\_certFacts}) and each band leaf, with directions given by dyadic coefficients, close to $u_L$ and $u_U$; \texttt{Agg.\allowbreak halfplane\_L\_of\_cover} and \texttt{Agg.\allowbreak halfplane\_U\_of\_cover} & the paper's\\\addlinespace[2pt] Proposition~\ref{prop:cert}(g) & none: (g) serves only the paragraph after Theorem~\ref{thm:N} & not used\\\addlinespace[2pt] Proposition~\ref{prop:cert}(h) and the leaves of type B of the umbilic cover, in Proposition~\ref{prop:classify}(c) & \texttt{Ex.\allowbreak Cusp.\allowbreak cuspRayCertFacts}: one certified point on each of the four families of mirror points in $W$, from a mirror solve in a fold leaf or from one of the band leaves \texttt{Band2.\allowbreak Test.\allowbreak bandA0} and \texttt{Band2.\allowbreak Test.\allowbreak bandA1} & different\\\addlinespace[2pt] the bound \eqref{eq:bandquant} of the leaves of type B, used as \eqref{eq:bandkappa} & \texttt{Agg.\allowbreak BandFacts}, from \texttt{Band2.\allowbreak bandLeaf\_facts2}, \texttt{Band2.\allowbreak bandLeaf\_facts3}, \texttt{Chart.\allowbreak topBand\_leaf\_ok} and \texttt{Chart.\allowbreak umbBand\_leaf\_ok}; \texttt{Agg.\allowbreak band\_of\_cover} combines the bounds as in the proof of Lemma~\ref{lem:cuspthree} & the paper's, along straight lines\\ \bottomrule \end{tabular} \par\vspace{6pt} \caption{The items of Proposition~\ref{prop:cert} and the other ingredients of Sections~\ref{sec:thm1} and~\ref{sec:critical} that rest on the certificates, and their counterparts in the formal proof. The Lean names are relative to the namespace \texttt{CC50}, and $M_{\mathrm C}$ is the compliance matrix of the remark on the sign of $J$ in the formal proof. ``The paper's'' means that the formal proof follows the argument of the paper, with certified quantities of its own.}\label{tab:formal} \end{table} \begin{remark*}[the sign of $J$ in the formal proof] For $a\in\Om$ place the configuration with $x_4=0$ and $x_1$, $x_2$, $x_3$ in counterclockwise order, and put $\beta_i=S_i/S$. Give each of its six segments $b$ a vector $\gamma_b\in\R^2$ and a weight $v_b$: for the spoke $i4$, $\gamma_b=g_i$ and $v_b=a_i^2(1-a_i^3)\beta_i$, and for the outer side $jk$, $\gamma_b=g_j+g_k$ and $v_b=R_i(R_i^{3/2}-1)\beta_j\beta_k$. Here $g_i=n_i/h_i$ is the gradient of $\log S_i$ with respect to $x_4$, where $n_i$ is the unit normal of the side $x_jx_k$ that points into the triangle and $h_i$ is the distance of $x_4$ from that side. The weights are positive, and the \emph{compliance matrix} \[ M_{\mathrm C}=\frac13\sum_bv_b\,(\gamma_b-\bar\gamma)(\gamma_b-\bar\gamma)^{\mathsf T},\qquad \bar\gamma=\frac{\sum_bv_b\gamma_b}{\sum_bv_b}, \] is a symmetric $2\times2$ matrix that depends on $a$ and $\theta$ but on no derivative. The formalization proves that on $\Om$ \[ J\,\det\Psi_{\mathrm C}\,\det\Lambda_{\mathrm C}=\det(I-M_{\mathrm C}),\qquad \det\Psi_{\mathrm C}<0<\det\Lambda_{\mathrm C}, \] hence $\operatorname{sign}J=-\operatorname{sign}\det(I-M_{\mathrm C})$ (theorems \texttt{CC50.\allowbreak Compliance.\allowbreak J\_mul\_det\_Psi\_mul\_det\_Lam}, \texttt{det\_PsiC\_neg}, \texttt{det\_LamC\_pos} and \texttt{sign\_J} in \texttt{CC50/\allowbreak Compliance/\allowbreak TheoremC.lean}). Here $\Lambda_{\mathrm C}$ maps $\varepsilon\in\R^3$ to $\bigl(\sum_l\varepsilon_lS_l,\ \sum_l\varepsilon_lS_lx_l\bigr)\in\R\times\R^2$, so that $\det\Lambda_{\mathrm C}=2S_1S_2S_3S$. The matrix $\Psi_{\mathrm C}$, \texttt{PsiC} in the same file, maps the three parameters of a load to the elongations of the spokes in the elastic response of the framework formed by the six segments, with stiffnesses that are positive where $K<0$. The proof has three steps. First, $M_{\mathrm C}$ is the compliance of this framework for the loads $S_1c$, $S_2c$, $S_3c$ and $-Sc$ on the four bodies, $c\in\R^2$, and an exact identity for the flexibility of a framework with one self-stress turns it into the covariance above. Second, for every configuration with body~$4$ strictly inside the triangle of the others and all positive stiffnesses, the matrix that takes the place of $\Psi_{\mathrm C}$ is invertible, and its determinant is negative, since these pairs form a connected set and the determinant is negative at one of them. Third, differentiating the CC equations along the family of configurations parametrized by $a$ gives a $3\times3$ matrix $\mathcal Q$ with $\Psi_{\mathrm C}\mathcal Q=I$ and $T\mathcal Q=\Lambda_{\mathrm C}\,\partial\mu/\partial a$, where $T$ is block triangular with $\det T=\det(I-M_{\mathrm C})$; taking determinants yields the identity. \end{remark*} Apart from the certificates, the formal proof follows Sections~\ref{sec:setup}--\ref{sec:hand} and~\ref{sec:thm1}--\ref{sec:degenerate} and, like Section~\ref{sec:thm1}, needs no degree theory; it derives Theorem~\ref{thm:N}(g), however, from $J<0$ at $s_{eq}(1,1,1)$ (Proposition~\ref{prop:ax}) and Theorem~\ref{thm:degtwo} instead of Table~\ref{tab:count}. Dziobek's relations, the absence of CCs with exactly three bodies collinear and the six convex CCs come from the formalization of \cite{Tom26}, which is part of the formal proof, and Moulton's count \cite{Mou10} is proved as well. The closed forms of the factors of $J$ on the axis (Proposition~\ref{prop:ax}) and the inequality $c(s^*)\ne0$ of Proposition~\ref{prop:U}, which the paper checks by computer algebra, are proved in Lean. The formal count at a cusp point (Proposition~\ref{prop:cuspcount}) needs $F$ only of class $C^3$, not real-analytic as in Lemma~\ref{lem:cuspnormal}(c). Besides Theorems~\ref{thm:count} and~\ref{thm:N}, the formalization proves Theorem~\ref{thm:family}, except the $45$-digit values of part~(3); for the digits printed in Theorem~\ref{thm:N}(e) it proves that $m^{**}$ and $m_f$ lie in the two intervals of width $5.4\cdot10^{-25}$ of Section~\ref{sec:famcount}. The formalization does not cover Section~\ref{sec:checks}, in particular the constant $\kappa_s$ and Proposition~\ref{prop:deltoid}. The README of the formalization lists the other differences from the paper. The code, the formalization and the data are released under the Apache License~2.0. \section*{Use of AI tools} Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to draft the text. \section*{Funding and competing interests} This research received no specific grant from any funding agency. The author has no competing interests to declare that are relevant to the content of this article. \begin{thebibliography}{CCLM15} \bibitem[ACS12]{ACS12} A.~Albouy, H.~E. Cabral and A.~A. Santos, \emph{Some problems on the classical $n$-body problem}, Celestial Mech. Dynam. Astronom. \textbf{113} (2012), 369--375. \bibitem[AFS08]{AFS08} A.~Albouy, Y.~Fu and S.~Sun, \emph{Symmetry of planar four-body convex central configurations}, Proc. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci. \textbf{464} (2008), 1355--1365. \bibitem[AK12]{AK12} A.~Albouy and V.~Kaloshin, \emph{Finiteness of central configurations of five bodies in the plane}, Ann. of Math. (2) \textbf{176} (2012), 535--588. \bibitem[Alb95]{Alb95} A.~Albouy, \emph{Sym\'etrie des configurations centrales de quatre corps}, C. R. Acad. Sci. Paris S\'er. I \textbf{320} (1995), 217--220. \bibitem[Alb96]{Alb96} A.~Albouy, \emph{The symmetric central configurations of four equal masses}, Contemp. Math. \textbf{198} (1996), 131--135. \bibitem[Bar08]{Bar08} J.~F. Barros, \emph{Configura\c{c}\~oes centrais no problema restrito dos 4-corpos no plano}, Ph.D. thesis, Universidade Federal de Pernambuco, Recife, 2008. \bibitem[BL11]{BL11} J.~F. Barros and E.~S.~G. Leandro, \emph{The set of degenerate central configurations in the planar restricted four-body problem}, SIAM J. Math. Anal. \textbf{43} (2011), 634--661. \bibitem[BL14]{BL14} J.~F. Barros and E.~S.~G. Leandro, \emph{Bifurcations and enumeration of classes of relative equilibria in the planar restricted four-body problem}, SIAM J. Math. Anal. \textbf{46} (2014), 1185--1203. \bibitem[BLP09]{BLP09} J.~Bernat, J.~Llibre and E.~P\'erez-Chavela, \emph{On the planar central configurations of the $4$-body problem with three equal masses}, Dyn. Contin. Discrete Impuls. Syst. Ser. A Math. Anal. \textbf{16} (2009), 1--13. \bibitem[CCLM15]{CCLM15} M.~Corbera, J.~M. Cors, J.~Llibre and R.~Moeckel, \emph{Bifurcation of relative equilibria of the $(1+3)$-body problem}, SIAM J. Math. Anal. \textbf{47} (2015), 1377--1404; preprint of December 3, 2014, \url{https://www-users.cse.umn.edu/~rmoeckel/research/Bifurcations1+3BP.9.pdf} (numbering of this preprint). \bibitem[CCR19]{CCR19} M.~Corbera, J.~M. Cors and G.~E. Roberts, \emph{Classifying four-body convex central configurations}, Celestial Mech. Dynam. Astronom. \textbf{131} (2019), Paper No.~34. \bibitem[Cha18]{Cha18} J.~Chazy, \emph{Sur certaines trajectoires du probl\`eme des $n$ corps}, Bull. Astron. \textbf{35} (1918), 321--389. \bibitem[dMU21]{dMU21} L.~de Moura and S.~Ullrich, \emph{The Lean~4 theorem prover and programming language}, in: Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. \textbf{12699}, Springer, Cham, 2021, 625--635. \bibitem[Dzi00]{Dzi00} O.~Dziobek, \emph{\"Uber einen merkw\"urdigen Fall des Vielk\"orperproblems}, Astron. Nachr. \textbf{152} (1900), 33--46. \bibitem[FLI25]{FLI25} The FLINT team, \emph{FLINT: Fast Library for Number Theory}, version 3.4.0, 2025, \url{https://flintlib.org}. \bibitem[FTZ24]{FTZ24} J.-Ll. Figueras, W.~Tucker and P.~Zgliczy\'nski, \emph{The number of relative equilibria in the PCR4BP}, J. Dynam. Differential Equations \textbf{36} (2024), 2827--2877. \bibitem[Ham02]{Ham02} M.~Hampton, \emph{Concave central configurations in the four-body problem}, Ph.D. thesis, University of Washington, Seattle, 2002. \bibitem[HM06]{HM06} M.~Hampton and R.~Moeckel, \emph{Finiteness of relative equilibria of the four-body problem}, Invent. Math. \textbf{163} (2006), 289--312; preprint of December 17, 2004, \url{https://www-users.cse.umn.edu/~rmoeckel/research/FinitenessRE4BP.rev.pdf} (numbering of this preprint). \bibitem[Joh17]{Joh17} F.~Johansson, \emph{Arb: efficient arbitrary-precision midpoint-radius interval arithmetic}, IEEE Trans. Comput. \textbf{66} (2017), 1281--1292. \bibitem[Kra69]{Kra69} R.~Krawczyk, \emph{Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken}, Computing \textbf{4} (1969), 187--201. \bibitem[Kul97]{Kul97} W.~Kulpa, \emph{The Poincar\'e--Miranda theorem}, Amer. Math. Monthly \textbf{104} (1997), 545--550. \bibitem[Lea03]{Lea03} E.~S.~G. Leandro, \emph{Finiteness and bifurcations of some symmetrical classes of central configurations}, Arch. Ration. Mech. Anal. \textbf{167} (2003), 147--177. \bibitem[LPRX26]{LPRX26} Y.~Liu, N.~Poudel, R.~Raut and Z.~Xie, \emph{Concave kite central configurations in the planar four-body problem with three equal masses}, arXiv:2606.19596 (2026). \bibitem[LS09]{LS09} T.-L. Lee and M.~Santoprete, \emph{Central configurations of the five-body problem with equal masses}, Celestial Mech. Dynam. Astronom. \textbf{104} (2009), 369--381. \bibitem[MB03]{MB03} K.~Makino and M.~Berz, \emph{Taylor models and other validated functional inclusion methods}, Int. J. Pure Appl. Math. \textbf{4} (2003), 379--456. \bibitem[MB32]{MB32} W.~D. MacMillan and W.~Bartky, \emph{Permanent configurations in the problem of four bodies}, Trans. Amer. Math. Soc. \textbf{34} (1932), 838--875. \bibitem[mC20]{mC20} The mathlib Community, \emph{The Lean mathematical library}, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367--381. \bibitem[Mir40]{Mir40} C.~Miranda, \emph{Un'osservazione su un teorema di Brouwer}, Boll. Un. Mat. Ital. (2) \textbf{3} (1940), 5--7. \bibitem[MKC09]{MKC09} R.~E. Moore, R.~B. Kearfott and M.~J. Cloud, \emph{Introduction to Interval Analysis}, SIAM, Philadelphia, PA, 2009. \bibitem[Moe01]{Moe01} R.~Moeckel, \emph{Generic finiteness for Dziobek configurations}, Trans. Amer. Math. Soc. \textbf{353} (2001), 4673--4686. \bibitem[Moe14]{Moe14} R.~Moeckel, \emph{Lectures on central configurations}, lecture notes of a course at the Centre de Recerca Matem\`atica, Barcelona, January 2014 (version of March 20, 2014), \url{https://www-users.cse.umn.edu/~rmoeckel/notes/CentralConfigurations.pdf}. \bibitem[Moe15]{Moe15} R.~Moeckel, \emph{Central configurations}, in: J.~Llibre, R.~Moeckel and C.~Sim\'o, Central Configurations, Periodic Orbits, and Hamiltonian Systems, Adv. Courses Math. CRM Barcelona, Birkh\"auser, 2015, 105--167. \bibitem[Moe90]{Moe90} R.~Moeckel, \emph{On central configurations}, Math. Z. \textbf{205} (1990), 499--517. \bibitem[Moo66]{Moo66} R.~E. Moore, \emph{Interval Analysis}, Prentice-Hall, Englewood Cliffs, NJ, 1966. \bibitem[Moo77]{Moo77} R.~E. Moore, \emph{A test for existence of solutions to nonlinear systems}, SIAM J. Numer. Anal. \textbf{14} (1977), 611--615. \bibitem[Mou10]{Mou10} F.~R. Moulton, \emph{The straight line solutions of the problem of $n$ bodies}, Ann. of Math. (2) \textbf{12} (1910), 1--17. \bibitem[mpm23]{mpm23} The mpmath development team, \emph{mpmath: a Python library for arbitrary-precision floating-point arithmetic (version 1.3.0)}, 2023, \url{http://mpmath.org/}. \bibitem[MS88]{MS88} K.~R. Meyer and D.~S. Schmidt, \emph{Bifurcations of relative equilibria in the $4$- and $5$-body problem}, Ergodic Theory Dynam. Systems \textbf{8$^*$} (1988), 215--225. \bibitem[MZ19]{MZ19} M.~Moczurad and P.~Zgliczy\'nski, \emph{Central configurations in planar $n$-body problem with equal masses for $n=5,6,7$}, Celestial Mech. Dynam. Astronom. \textbf{131} (2019), Paper No.~46. \bibitem[Neu90]{Neu90} A.~Neumaier, \emph{Interval Methods for Systems of Equations}, Encyclopedia Math. Appl. \textbf{37}, Cambridge Univ. Press, Cambridge, 1990. \bibitem[Pal73]{PalT} J.~I. Palmore, \emph{Relative equilibria of the $n$-body problem}, Ph.D. thesis, University of California, Berkeley, 1973. \bibitem[Pal75]{PalII} J.~I. Palmore, \emph{Classifying relative equilibria.~II}, Bull. Amer. Math. Soc. \textbf{81} (1975), 489--491. \bibitem[Rob25]{Rob24} G.~E. Roberts, \emph{On kite central configurations}, Nonlinearity \textbf{38} (2025), no.~7, Paper No.~075001, arXiv:2411.07867. \bibitem[RS16]{RS16} D.~Rusu and M.~Santoprete, \emph{Bifurcations of central configurations in the four-body problem with some equal masses}, SIAM J. Appl. Dyn. Syst. \textbf{15} (2016), 440--458, arXiv:1412.6443 (numbering of the arXiv version). \bibitem[Sar42]{Sar42} A.~Sard, \emph{The measure of the critical values of differentiable maps}, Bull. Amer. Math. Soc. \textbf{48} (1942), 883--890. \bibitem[SX10]{SX10} J.~Shi and Z.~Xie, \emph{Classification of four-body central configurations with three equal masses}, J. Math. Anal. Appl. \textbf{363} (2010), 512--524. \bibitem[Shu71]{Shu71} M.~Shub, \emph{Appendix to Smale's paper: Diagonals and relative equilibria}, in: Manifolds--Amsterdam 1970, Lecture Notes in Math. \textbf{197}, Springer, 1971, 199--201. \bibitem[Sim78]{Sim78} C.~Sim\'o, \emph{Relative equilibrium solutions in the four body problem}, Celestial Mech. \textbf{18} (1978), 165--184. \bibitem[Sma98]{Sma98} S.~Smale, \emph{Mathematical problems for the next century}, Math. Intelligencer \textbf{20} (1998), 7--15. \bibitem[SXY25]{SXY25} S.~Sun, Z.~Xie and P.~You, \emph{Degeneracy of planar central configurations in the $N$-body problem}, arXiv:2510.25649 (2025). \bibitem[Tom26]{Tom26} T.~S. Tomar, \emph{Uniqueness of four-body convex central configurations for all masses}, arXiv:2609.35632 (2026); Zenodo, \href{https://doi.org/10.5281/zenodo.23004306}{doi:10.5281/zenodo.23004306} (all versions). \bibitem[Tuc11]{Tuc11} W.~Tucker, \emph{Validated Numerics: A Short Introduction to Rigorous Computations}, Princeton Univ. Press, Princeton, NJ, 2011. \bibitem[Whi55]{Whi55} H.~Whitney, \emph{On singularities of mappings of Euclidean spaces. I. Mappings of the plane into the plane}, Ann. of Math. (2) \textbf{62} (1955), 374--410. \bibitem[Win41]{Win41} A.~Wintner, \emph{The Analytical Foundations of Celestial Mechanics}, Princeton Math. Ser. \textbf{5}, Princeton Univ. Press, Princeton, NJ, 1941. \bibitem[Xia04]{Xia04} Z.~Xia, \emph{Convex central configurations for the $n$-body problem}, J. Differential Equations \textbf{200} (2004), 185--190. \bibitem[ZX26]{ZX26} T.~Zhou and Z.~Xia, \emph{On the degeneracy of the central configuration formed by a regular $n$-gon with a central mass}, arXiv:2604.04610 (2026). \end{thebibliography} \end{document}