\documentclass[11pt]{amsart}
\usepackage[margin=1.1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{graphicx,booktabs,enumitem}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Uniqueness of four-body convex central configurations for all masses},
  pdfauthor={Tejasvi Singh Tomar}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{conjecture}[theorem]{Conjecture}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\theoremstyle{plain}
\newtheorem*{thmA}{Theorem A}
\newtheorem*{thmB}{Theorem B}
\newtheorem*{corC}{Corollary C}
\newtheorem*{corD}{Corollary D}
\numberwithin{equation}{section}
\setlength{\emergencystretch}{2em}

\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathbb{C}}
\newcommand{\dr}{\mathrm{d}r}
\DeclareMathOperator{\tr}{tr}
\DeclareMathOperator{\ind}{ind}
\newcommand{\lmax}{\lambda_{\max}}
\newcommand{\cS}{\mathcal{S}}
\newcommand{\cC}{\mathcal{C}}
\newcommand{\cE}{\mathcal{E}}
\newcommand{\cX}{\mathcal{X}}
\newcommand{\cZ}{\mathcal{Z}}
\newcommand{\cT}{\mathcal{T}}
\newcommand{\ip}[2]{\langle #1,#2\rangle}
\newcommand{\hA}{\widehat A}
\newcommand{\he}{\hat\eta}
\newcommand{\hw}{\hat w}

\begin{document}

\title[Uniqueness of four-body convex central configurations for all masses]{Uniqueness of four-body convex central\\ configurations for all masses}
\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, 58K05, 65G40}
\keywords{Central configurations, four-body problem, relative equilibria, uniqueness, nondegeneracy, Morse index, computer-assisted proof, interval arithmetic}

\begin{abstract}
We prove that for every choice of four positive masses and every cyclic ordering of the bodies there is exactly one strictly convex planar central configuration with that ordering, up to similarity. This answers Problem~10 in the list of Albouy, Cabral and Santos, which Santoprete calls the Simó--Yoccoz conjecture. The main step is a uniform lower bound for the Hessian at convex central configurations: it is at least one quarter of its radial part, which vanishes only on translations and rotations. Dziobek's relations turn the indefinite part of the Hessian into a negative multiple of a square, and a Cauchy--Schwarz argument bounds this term by the radial part times the trace of an explicit $2\times2$ matrix in which the masses do not appear. We prove that this trace is less than $\frac34$ by interval arithmetic on the three-dimensional set of normalized convex central configurations, in the coordinates of Corbera, Cors and Roberts. Uniqueness then follows by a covering argument from the case of four equal masses. The computation has been repeated with a second, independently written program. The Hessian bound and the uniqueness theorem, including the computation, have been formalized in the Lean proof assistant and checked by its kernel, using only the standard axioms. As consequences, every degenerate four-body central configuration is concave, the convex central configuration depends analytically on the masses, and the known symmetry theorems for kites, isosceles trapezoids and rhombi follow in a few lines. The analytic dependence and the symmetry theorems are also formalized.
\end{abstract}

\maketitle

\section{Introduction}\label{sec:intro}

\subsection{Central configurations}
Consider four bodies with masses $m_1,\dots,m_4>0$ and positions $q_1,\dots,q_4\in\R^2$. Write $q=(q_1,\dots,q_4)\in(\R^2)^4\cong\R^8$ and $r_{ij}=|q_i-q_j|$, and set
\[
U(q)=\sum_{i<j}\frac{m_im_j}{r_{ij}},\qquad M=\sum_i m_i,\qquad c=\frac1M\sum_i m_iq_i,\qquad I(q)=\sum_i m_i|q_i-c|^2 .
\]
A collision-free configuration $q$ is a \emph{central configuration} (CC) if
\begin{equation}\label{eq:cc}
\nabla_{q_i}U(q)+\lambda\,m_i(q_i-c)=0,\qquad i=1,\dots,4,
\end{equation}
for some $\lambda\in\R$. Pairing \eqref{eq:cc} with $q-c$ and using that $U$ is homogeneous of degree $-1$ and translation invariant shows that necessarily $\lambda=U(q)/I(q)>0$.
Central configurations are the configurations that admit homographic motions. In the plane, each CC generates a relative equilibrium of the Newtonian four-body problem, that is, a solution that rotates rigidly about the centre of mass. The set of CCs is invariant under the similarities of the plane (translations, rotations, dilations and reflections), and CCs are counted modulo similarity. General references are \cite{Moe15,Sma70}.

A planar four-body CC is either collinear or has no three bodies on a line (Lemma~\ref{lem:nocollinear}). In the second case it is either \emph{convex}, meaning that the bodies are the vertices of a strictly convex quadrilateral, or \emph{concave}, meaning that one body lies in the interior of the triangle formed by the other three. A convex configuration determines the cyclic order of the bodies along its boundary, up to reversal. Four labelled bodies have three such cyclic orders, represented by $(1234)$, $(1243)$ and $(1324)$.

MacMillan and Bartky \cite{MB32} proved that for every choice of masses and each cyclic order there is a convex CC with that cyclic order. Xia \cite{Xia04} gave a simpler proof, and a variational proof is given in \cite{Moe15}. Albouy, Fu and Sun conjectured that this convex CC is unique for every choice of positive masses \cite{AFS08}. Albouy, Cabral and Santos included the question in their list of open problems on the classical $n$-body problem, asking whether, for the Newtonian potential, the convex CC with a given cyclic order is unique up to similarity \cite[Problem~10]{ACS12}. At that time uniqueness was known when the two bodies at the ends of a diagonal have equal masses, while the case of two pairs of equal masses at adjacent vertices was still open. Santoprete \cite{San26} calls the expected positive answer the Simó--Yoccoz conjecture. The number of four-body CCs as a function of the masses was explored numerically by Simó \cite{Sim78}.

\subsection{Previous results}
Uniqueness had been established in the following cases.
\begin{itemize}[leftmargin=2em]
\item \emph{Equal masses.} Albouy \cite{Alb95,Alb96} proved that every CC of four equal masses has an axis of symmetry and classified them all. In particular the only convex one is the square.
\item \emph{Equal masses at the ends of a diagonal.} Here the convex CC is symmetric with respect to the other diagonal \cite{LS02,PCS07,AFS08}. Uniqueness then follows from Leandro's analysis of kite configurations \cite{Lea03}. Roberts \cite{Rob25} gave a new proof of the uniqueness of convex kites, based on the Poincaré--Hopf theorem.
\item \emph{Two pairs of equal masses at adjacent vertices.} Fernandes, Llibre and Mello \cite{FLM17} proved that the isosceles trapezoid is the unique convex CC; see also \cite{Xie12}.
\item \emph{Restricted classes.} Santoprete proved uniqueness among co-circular CCs \cite{San21a} and among trapezoidal CCs \cite{San21b}; these classes are studied in \cite{CR12,CCLP19}. Corbera, Cors and Roberts showed that a convex CC with perpendicular diagonals is a kite \cite{CCR18}.
\item \emph{Small masses.} Uniqueness holds when three of the masses are sufficiently small \cite{CCLM15}.
\item \emph{A region of masses.} Sun, Xie and You \cite{SXY23} proved uniqueness by interval arithmetic for $m_2=1$ the largest mass and $(m_1,m_3,m_4)\in[0.6,1]^3$.
\end{itemize}
Corbera, Cors and Roberts \cite{CCR19} described the set of convex CCs, normalized and ordered as in Section~\ref{sec:normal}, as a graph over an explicit three-dimensional domain. They expressed the hope that the normalized mass map on this domain is injective, which would prove uniqueness. Santoprete \cite{San26} decomposed the constrained Hessian at a planar CC into a positive semidefinite part and a signed part of rank two. Santoprete characterized definiteness by an explicit $2\times2$ eigenvalue problem, and pointed out that if all convex CCs with a given ordering were nondegenerate minima, Morse-theoretic arguments could yield uniqueness. That approach had been carried out within the co-circular and trapezoidal classes \cite{San21a,San21b}, and for kites in \cite{Rob25}. Sun, Xie and You \cite[Theorem~4.1]{SXY25} proved by interval arithmetic that rhombus CCs are nondegenerate, and Santoprete \cite[Proposition~7.1]{San26} showed that their Morse index is $0$.

Concave CCs exist for all masses \cite{Ham02}, but they are not unique. There are degenerate concave kites and fold bifurcations, and the number of concave kites for given masses can be $0$, $1$ or $2$ \cite{Rob25,LX25,LPRX26}. Hampton and Moeckel proved that the number of four-body CCs is finite \cite{HM06}; see \cite{AK12} for five bodies and \cite{Moe01} for Dziobek configurations.

\subsection{Results}
We say that a CC is \emph{nondegenerate} if its similarity class is a nondegenerate critical point of $UI^{1/2}$ on the shape space (Section~\ref{sec:shape}). This agrees with the definition used in \cite{Moe15,Pac87}.

\begin{thmA}
Let $m_1,\dots,m_4>0$. For each cyclic order of the four bodies there is exactly one convex central configuration with that cyclic order, up to similarity. It is a nondegenerate local minimum of $UI^{1/2}$ on the shape space, and it depends real-analytically on the masses.
\end{thmA}

Up to orientation-preserving similarities there are exactly two such configurations, and they are mirror images of each other. Theorem~A rests on a quantitative nondegeneracy statement. For a CC $q$ let
\[
Q(v)=D^2\Bigl(U+\frac{\lambda}{2}I\Bigr)(q)[v,v],\qquad v=(v_1,\dots,v_4)\in(\R^2)^4,
\]
where $\lambda=U(q)/I(q)$ is held fixed, and let
\[
K(v)=\sum_{i<j}\frac{3m_im_j}{r_{ij}^3}\Bigl(\frac{\ip{q_i-q_j}{v_i-v_j}}{r_{ij}}\Bigr)^{2}.
\]
Thus $Q$ is the Hessian of the Lagrange function for the extremal problem ``$U$ restricted to a level set of $I$'', and $K\ge0$ is the part of $Q$ that comes from the second derivatives of the pair potentials in the radial directions (Lemma~\ref{lem:hessian}). By infinitesimal rigidity, $K(v)=0$ if and only if $v$ is an infinitesimal translation or rotation (Lemma~\ref{lem:rigid}).

\begin{thmB}
At every convex central configuration of four bodies,
\[
Q(v)\ \ge\ \tfrac14\,K(v)\qquad\text{for all }v\in(\R^2)^4 .
\]
In particular every convex central configuration is nondegenerate and has Morse index $0$.
\end{thmB}

\begin{corC}
Fix positive masses $m_1,\dots,m_4$.
\begin{enumerate}[label=\textup{(\roman*)},leftmargin=2.2em]
\item For each cyclic order and orientation, the convex CC, as a point of shape space, is a real-analytic function of the masses.
\item In the coordinates of Corbera, Cors and Roberts, the normalized mass map on the set of normalized convex CCs is injective. This is the property that \cite{CCR19} hoped to establish.
\item There are exactly three convex CCs up to similarity, and exactly six up to orientation-preserving similarity. All of them are nondegenerate local minima of $UI^{1/2}$. Consequently, the Morse-theoretic lower bound of $34$ planar CCs up to orientation-preserving similarity \cite{Moe15} holds for every choice of masses for which the concave CCs are nondegenerate.
\item Every degenerate planar four-body CC is concave.
\end{enumerate}
\end{corC}

Uniqueness also recovers the known symmetry theorems. Their earlier proofs rely on a detailed analysis of the Dziobek equations; here they follow in a few lines.

\begin{corD}
Label the bodies so that the cyclic order is $(1234)$, and let $q$ be the convex CC.
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2.2em]
\item If $m_1=m_3$, then $q$ is symmetric with respect to the diagonal $q_2q_4$ \textup{\cite{AFS08}}.
\item If $m_1=m_2$ and $m_3=m_4$, then $q$ is an isosceles trapezoid with $q_1q_2\parallel q_3q_4$ \textup{\cite{FLM17}}.
\item If $m_1=m_3$ and $m_2=m_4$, then $q$ is a rhombus \textup{\cite{LS02,PCS07,AFS08}}.
\end{enumerate}
\end{corD}

The constant $\frac14$ in Theorem~B is not optimal: the second implementation of the computation, described in Section~\ref{sec:indep}, gives $Q\ge\frac{13}{32}K$. In the other direction, the best constant is at most $\frac23$: along a family of convex CCs in which two of the masses tend to zero, the smallest generalized eigenvalue of the pair $(Q,K)$ tends to $\frac23$ (Proposition~\ref{prop:corner}). Numerically $\frac23$ is the optimal constant (Conjecture~\ref{conj:sharp}).

\subsection{Method}
The route from nondegeneracy to uniqueness is well known \cite{San21a,San21b,Rob25,San26}. If every convex CC with a given cyclic order is a nondegenerate minimum, then a degree or Morse-theoretic argument shows that their number does not depend on the masses, and for equal masses it is one. The difficulty is to prove nondegeneracy for all masses at once. Our proof of Theorem~B has three ingredients.

\emph{An identity.} Dziobek's relations $m_im_j(r_{ij}^{-3}-\lambda/M)=\sigma A_iA_j$, where the $A_l$ are oriented triangle areas and $\sigma<0$, turn the indefinite part of $Q$ into a negative multiple of a square:
\[
Q=K-|\sigma|\,|L|^2,\qquad L(v)=\sum_{l=1}^4A_lv_l\in\R^2
\]
(Proposition~\ref{prop:identity}). We found this identity independently of \cite{San26}. It is the analogue, in the coordinates of the bodies, of Santoprete's decomposition in pair space (Remark~\ref{rem:identity}).

\emph{A majorant in which the masses do not appear.} We express $L$ through the variations of the mutual distances and apply the Cauchy--Schwarz inequality against $K$. This gives $|\sigma|\,|L|^2\le\tr S(y)\,K$ for every $y\in\R^2$, where $S(y)$ is an explicit positive semidefinite $2\times2$ matrix that depends only on the shape of the configuration (Proposition~\ref{prop:majorant}). Since the shape of a convex CC in turn determines the masses, the problem becomes the estimation of an explicit function on the three-dimensional set $\cE$ of normalized convex CCs, which \cite{CCR19} describe by a single analytic equation in four explicit coordinates.

\emph{A rigorous computation.} We cover $\cE$ by boxes, localize it with interval Newton steps applied to the Dziobek equation, and bound $\tr S(y)$ by $\frac34$ on every box, using ball arithmetic. The set $\cE$ is not compact: as two of the masses tend to zero, the configuration degenerates, and the two remaining bodies and the point where the two small bodies collide form an equilateral triangle. We handle this end with a blow-up chart in which $\cE$ extends analytically across the corner. At the corner the smallest generalized eigenvalue of $(Q,K)$ has limits between $\frac23$ and $\frac34$ (Proposition~\ref{prop:corner}), which leaves room for a uniform estimate. With $32$ processes the computation takes under five minutes (Section~\ref{sec:results}). A second program, written from a specification of the formulas without access to the code of the first, repeats it (Section~\ref{sec:indep}).

Theorem~A follows from Theorem~B by a covering argument. The pairs (convex shape, masses) that form CCs make up a manifold, and by Theorem~B its projection to the simplex of masses is a local diffeomorphism. The projection is also proper, because limits of convex CCs are convex: Shub's lemma excludes collisions, and Theorem~B, applied once more, excludes collinear limits (Lemma~\ref{lem:collinear}). So the projection is a covering map, and we compute its degree at equal masses, where the symmetry theorem of Albouy, Fu and Sun \cite{AFS08} shows that the square is the only convex CC.

Both theorems, including the computation, have also been formalized in the Lean proof assistant, together with Corollary~D, most of Corollary~C and most of the preliminaries. The formal proof is checked by Lean's kernel and uses only the standard axioms. Section~\ref{sec:lean} describes it and lists what is not formalized.

\subsection{Organization}
Section~\ref{sec:prelim} collects the preliminaries: the equations, the Hessian, the shape space, oriented areas and Dziobek's relations. Section~\ref{sec:identity} proves the identity and the majorant. Section~\ref{sec:normal} introduces the normalized coordinates, the a priori bounds and the blow-up chart. Section~\ref{sec:cap} describes the computer-assisted proof of the bound $\tr S<\frac34$ and a second implementation of it. Section~\ref{sec:proofs} proves Theorems~B and~A and describes their formalization in Lean, and Section~\ref{sec:cons} proves the corollaries and states some open questions. \hyperref[app:chart]{The Appendix} lists the formulas of the blow-up chart.

\section{Preliminaries}\label{sec:prelim}

Throughout, $m_1,\dots,m_4>0$. The six unordered pairs $e=ij$, $1\le i<j\le4$, are called \emph{edges}. For an edge $e=ij$ we write $q_e=q_i-q_j$, $v_e=v_i-v_j$, $r_e=|q_e|$, $R_e=r_e^2$ and $s_e=r_e^{-3}$. We identify $\R^2$ with $\C$, write $J$ for multiplication by $\sqrt{-1}$ (rotation by $\pi/2$), and let $J$ act diagonally on $(\R^2)^4=\C^4$. The mass inner product is $\ip{u}{v}_M=\sum_im_i\ip{u_i}{v_i}$.

\subsection{The equations and the Hessian}
Let $q$ be a CC with multiplier $\lambda=U/I$, and set
\[
\lambda'=\frac{\lambda}{M},\qquad w_e=s_e-\lambda',\qquad \omega_e=m_im_jw_e\quad(e=ij).
\]
Since $\nabla_{q_i}U=\sum_{j\ne i}m_im_js_{ij}(q_j-q_i)$ and $m_i(q_i-c)=-\frac1M\sum_{j}m_im_j(q_j-q_i)$, equation \eqref{eq:cc} is equivalent to
\begin{equation}\label{eq:equil}
\sum_{j\ne i}\omega_{ij}\,(q_j-q_i)=0,\qquad i=1,\dots,4 .
\end{equation}
Conversely, if a collision-free $q$ satisfies \eqref{eq:equil} for some $\lambda'\in\R$, then $q$ satisfies \eqref{eq:cc} with $\lambda=M\lambda'$. Pairing with $q-c$ then shows that $\lambda=U/I$, so $q$ is a CC.

Because $I=\frac1M\sum_{i<j}m_im_jr_{ij}^2$, the function $\Phi=U+\frac{\lambda}{2}I$, with $\lambda$ frozen at its value at $q$, is a sum of pair potentials:
\[
\Phi=\sum_{i<j}m_im_j\,\varphi(r_{ij}),\qquad \varphi(r)=\frac1r+\frac{\lambda'}{2}r^2 .
\]
One computes $\varphi'(r)/r=-(r^{-3}-\lambda')$ and $\varphi''(r)-\varphi'(r)/r=3r^{-3}$. For an edge $e$ and a vector $v\in(\R^2)^4$ let
\[
\dr_e(v)=\frac{\ip{q_e}{v_e}}{r_e}
\]
be the first variation of $r_e$, and put $\kappa_e=3m_im_js_e>0$ for $e=ij$.

\begin{lemma}\label{lem:hessian}
Let $q$ be a CC and $Q=D^2\Phi(q)$. Then:
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item $Q(v)=K(v)-\sum_e\omega_e|v_e|^2$, where $K(v)=\sum_e\kappa_e\,\dr_e(v)^2$;
\item $Q(q,v)=3\lambda\ip{q-c}{v}_M$ for all $v$, and in particular $Q(q,q)=3U$;
\item the three-dimensional space $\cT$ spanned by the translations and by $J(q-c)$ is contained in $\ker Q$.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) For $x\in\R^2\setminus\{0\}$ the Hessian of $x\mapsto\varphi(|x|)$ is $\varphi''\,\hat x\hat x^{\mathsf T}+\frac{\varphi'}{r}(\mathrm{Id}-\hat x\hat x^{\mathsf T})=(\varphi''-\frac{\varphi'}{r})\hat x\hat x^{\mathsf T}+\frac{\varphi'}{r}\mathrm{Id}$, where $r=|x|$ and $\hat x=x/r$. Evaluating at $x=q_e$ in the direction $v_e$ and summing over the edges gives (a).
(b) Since $U$ is homogeneous of degree $-1$, $\nabla U$ is homogeneous of degree $-2$, so $D^2U(q)[q,v]=-2\ip{\nabla U(q)}{v}=2\lambda\ip{q-c}{v}_M$ by \eqref{eq:cc}. Also $D^2I(q)[u,v]=2\ip{u-\bar u}{v-\bar v}_M$, where $\bar u=\frac1M\sum_im_iu_i$, so $\frac\lambda2D^2I(q)[q,v]=\lambda\ip{q-c}{v}_M$. Adding gives $Q(q,v)=3\lambda\ip{q-c}{v}_M$, and $Q(q,q)=3\lambda I=3U$.
(c) $\Phi$ is invariant under translations and rotations. Differentiating the identities $\Phi(q+t)=\Phi(q)$ and $\nabla\Phi(e^{J\theta}q)=e^{J\theta}\nabla\Phi(q)$ at a critical point of $\Phi$ shows that translations and $Jq$ lie in $\ker Q$. Since $J(q-c)$ differs from $Jq$ by a translation, the claim follows.
\end{proof}

Moeckel \cite{Moe15} writes the same quadratic form, restricted to the normalized configuration space, as $H(x)$. In Moeckel's convention convex CCs are local minima and collinear CCs have index $n-2$.

\subsection{Shape space}\label{sec:shape}
Orientation-preserving similarities act on $\C^4$ by $q\mapsto\mu q+t\mathbb 1$, with $\mu\in\C^*$, $t\in\C$ and $\mathbb 1=(1,1,1,1)$. The quotient of the set of configurations that are not totally collapsed is the \emph{shape space}
\[
\cS=\mathbb P(\C^4/\C\mathbb 1)\cong\C P^2,
\]
a compact real four-manifold. For $i\ne j$, the normalization $q_i=0$, $q_j=1$ identifies the open set of classes with $q_i\ne q_j$ with $\C^2$, and these affine charts cover $\cS$. Let $\Delta\subset\cS$ be the collision locus, where $q_i=q_j$ for some $i\ne j$. Since $U(\mu q+t\mathbb 1)=|\mu|^{-1}U(q)$ and $I(\mu q+t\mathbb 1)=|\mu|^2I(q)$, the function
\[
f_m=U\,I^{1/2}
\]
descends to a real-analytic function on $\cS\setminus\Delta$. From $d(UI^{1/2})=I^{1/2}\bigl(dU+\frac{U}{2I}dI\bigr)$ we see that $[q]$ is a critical point of $f_m$ if and only if $q$ is a CC. We call a CC \emph{nondegenerate} if $[q]$ is a nondegenerate critical point of $f_m$, and define its \emph{Morse index} to be the index of $D^2f_m([q])$, where the \emph{index} of a quadratic form is the largest dimension of a subspace on which it is negative definite. Scaling all masses by the same factor multiplies $f_m$ by a constant, so the critical points depend only on the normalized masses.

\begin{lemma}\label{lem:shape}
Let $q$ be a CC and let $W$ be the space of vectors $v$ with $\sum_im_iv_i=0$, $\ip{q-c}{v}_M=0$ and $\ip{J(q-c)}{v}_M=0$. Then $(\R^2)^4=\cT\oplus\R(q-c)\oplus W$, the three summands are $Q$-orthogonal, and $Q(q-c)=3U>0$. The differential of $q\mapsto[q]$ maps $W$ isomorphically onto $T_{[q]}\cS$, and under this isomorphism $D^2f_m([q])$ corresponds to $I^{1/2}\,Q|_W$. Consequently the Morse index of $q$ is the index of $Q$, and $q$ is nondegenerate if and only if $\ker Q=\cT$. In particular $q$ is a nondegenerate local minimum of $f_m$ if and only if $Q(v)>0$ for every $v\notin\cT$.
\end{lemma}

\begin{proof}
The translations are $\ip{\cdot}{\cdot}_M$-orthogonal to the vectors with $\sum_im_iv_i=0$, and $q-c$, $J(q-c)$ are $\ip{\cdot}{\cdot}_M$-orthogonal to each other. This gives the direct sum decomposition. The space $\cT\oplus\R(q-c)$ is the tangent space at $q$ of the orbit of the similarity group, and $\dim W=4=\dim\cS$, so the differential of the projection maps $W$ isomorphically onto $T_{[q]}\cS$. The summand $\cT$ is $Q$-orthogonal to everything by Lemma~\ref{lem:hessian}(c). For $w\in W$, Lemma~\ref{lem:hessian}(b) gives $Q(q-c,w)=Q(q,w)=3\lambda\ip{q-c}{w}_M=0$. It also gives $Q(q-c)=Q(q)=3U$. Finally, differentiating $F=UI^{1/2}$ twice at a critical point, and using $dU=-\frac{U}{2I}dI$ there, gives
\[
D^2F(q)=I^{1/2}\Bigl[Q-\frac{3U}{4I^2}\,dI\otimes dI\Bigr].
\]
Here $dI(w)=2\ip{q-c}{w}_M=0$ for $w\in W$. Since $[q]$ is a critical point, $D^2f_m([q])$ evaluated on the image of $w$ equals $D^2F(q)[w,w]$.
\end{proof}

\subsection{Oriented areas}
For three points put $[ijk]=\frac12\det(q_j-q_i,\,q_k-q_i)$, and define
\[
A_1=[234],\qquad A_2=-[134],\qquad A_3=[124],\qquad A_4=-[123].
\]
For the square $q=(1,J,-1,-J)$, whose vertices are in counterclockwise order, the areas are $A_1=A_3=1$ and $A_2=A_4=-1$.

\begin{lemma}\label{lem:areas}
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item $\sum_lA_l=0$ and $\sum_lA_lq_l=0$.
\item $A_l(\mu q+t\mathbb 1)=|\mu|^2A_l(q)$ for $\mu\in\C^*$, $t\in\C$, and $A_l(\bar q)=-A_l(q)$.
\item If $q_i=q_j$ with $i\ne j$, then $A_k=0$ for $k\notin\{i,j\}$. If the $q_l$ are not all equal, then all $A_l$ vanish if and only if the four points are collinear.
\item Suppose that no three of the $q_l$ are collinear. Then every $A_l$ is nonzero, and exactly one of the following holds.
\begin{itemize}
\item Two of the $A_l$ are positive and two are negative. Then $q$ is a strictly convex quadrilateral whose diagonals join the two bodies with positive $A_l$ and the two bodies with negative $A_l$. The sign pattern $(+,-,+,-)$ occurs if and only if $q_1,q_2,q_3,q_4$ are the vertices of a strictly convex quadrilateral in counterclockwise order.
\item Three of the $A_l$ have the same sign. Then $q$ is concave, and the body whose $A_l$ has the other sign lies in the interior of the triangle formed by the other three.
\end{itemize}
\end{enumerate}
\end{lemma}

\begin{proof}
(a) Consider the $4\times4$ matrix whose columns are $(1,q_l)^{\mathsf T}\in\R^3$ together with a fourth row that repeats one of its three rows. Its determinant vanishes. Expanding along the repeated row gives $\sum_l(-1)^{l+1}\,2[\,\cdot\,]_l\,(1,q_l)=0$, where $[\,\cdot\,]_l$ is the triangle formed by the bodies other than $l$. This is the statement $\sum_lA_l(1,q_l)=0$.
(b) Complex multiplication by $\mu$ is a rotation composed with a dilation by $|\mu|$, and conjugation is a reflection.
(c) The first statement is clear. If not all points coincide, choose $q_i\ne q_j$. If all $A_l$ vanish, the two triangles containing $q_i$ and $q_j$ are degenerate, so all points lie on the line through $q_i$ and $q_j$.
(d) The $A_l$ are nonzero because no triangle is degenerate. Let $S$ be the sum of the positive $A_l$. By (a), $S$ is also the sum of the absolute values of the negative $A_l$, and
\[
p=\frac1S\sum_{A_l>0}A_lq_l=\frac1S\sum_{A_l<0}|A_l|q_l .
\]
If two of the $A_l$ are positive, $p$ lies in the open segment joining the two corresponding points and also in the open segment joining the other two. Two segments that cross at interior points are the diagonals of a convex quadrilateral, which is strictly convex because no three points are collinear. If three $A_l$ are positive, $p$ is the fourth point and is a convex combination of the other three with positive weights. For the pattern $(+,-,+,-)$ the diagonals are $q_1q_3$ and $q_2q_4$, so the cyclic order is $(1234)$. Moreover $A_1=[234]>0$ means that the triangle $q_2q_3q_4$ is positively oriented, that is, the quadrilateral is traversed counterclockwise. Conversely, let $q_1q_2q_3q_4$ be a counterclockwise strictly convex quadrilateral. No vertex lies inside the triangle of the others, so two $A_l$ are positive and two are negative, and the equal-sign pairs are the diagonals $\{1,3\}$ and $\{2,4\}$. Finally $A_1=[234]>0$, because three consecutive vertices of a counterclockwise convex polygon form a positively oriented triangle.
\end{proof}

\subsection{Infinitesimal rigidity}
Let $\dr:(\R^2)^4\to\R^6$ be the linear map $v\mapsto(\dr_e(v))_e$. A vector $(\omega_e)\in\R^6$ satisfying \eqref{eq:equil} is called a \emph{self-stress} of $q$. For $\omega\in\R^6$ and $v\in(\R^2)^4$,
\begin{equation}\label{eq:stressdual}
\sum_e\omega_er_e\,\dr_e(v)=\sum_{i<j}\omega_{ij}\ip{q_i-q_j}{v_i-v_j}=-\sum_i\Bigl\langle v_i,\sum_{j\ne i}\omega_{ij}(q_j-q_i)\Bigr\rangle .
\end{equation}

\begin{lemma}\label{lem:rigid}
Suppose that no three of $q_1,\dots,q_4$ are collinear. Then $\ker\dr$ is the space $\cT$ of infinitesimal translations and rotations, $\dr$ has rank $5$, and the self-stresses of $q$ are the multiples of $(A_iA_j)_{ij}$. The image of $\dr$ is the hyperplane $\tau^\perp$, where
\[
\tau_e=A_iA_j\,r_e\qquad(e=ij).
\]
In particular, if $q$ is a CC then $K(v)=0$ if and only if $v\in\cT$.
\end{lemma}

\begin{proof}
Let $v\in\ker\dr$. The triangle $q_1q_2q_3$ is nondegenerate, hence infinitesimally rigid. After subtracting an element of $\cT$ we may therefore assume $v_1=v_2=v_3=0$. Then $\ip{q_4-q_i}{v_4}=0$ for $i=1,2$. The vectors $q_4-q_1$ and $q_4-q_2$ span $\R^2$, so $v_4=0$. Hence $\ker\dr=\cT$ and $\dr$ has rank $5$. By \eqref{eq:stressdual}, $\omega$ is a self-stress if and only if $(\omega_er_e)_e$ is orthogonal to the image of $\dr$, which is a hyperplane. So the self-stresses form a line. By Lemma~\ref{lem:areas}(a),
\[
\sum_{j\ne i}A_iA_j(q_j-q_i)=A_i\Bigl(\sum_jA_jq_j-q_i\sum_jA_j\Bigr)=0,
\]
so $(A_iA_j)$ is a self-stress, and it is nonzero. Therefore $\operatorname{im}\dr=\tau^\perp$. The last statement follows because all $\kappa_e>0$.
\end{proof}

\subsection{Dziobek's relations}

\begin{lemma}\label{lem:nocollinear}
A planar CC of four bodies is either collinear or has no three bodies on a line.
\end{lemma}

\begin{proof}
Suppose that $q_1,q_2,q_3$ lie on a line $\ell$ and $q_4\notin\ell$, and let $n$ be a unit normal to $\ell$. For $i\le3$, pairing \eqref{eq:equil} with $n$ gives $\omega_{i4}\ip{q_4-q_i}{n}=0$. Since $\ip{q_4-q_i}{n}\ne0$, we get $w_{i4}=0$, that is, $r_{14}=r_{24}=r_{34}=\lambda'^{-1/3}$. Then the three distinct points $q_1,q_2,q_3$ of $\ell$ lie on a circle centred at $q_4$, which is impossible.
\end{proof}

\begin{lemma}[Dziobek \cite{Dzi00}]\label{lem:dziobek}
Let $q$ be a noncollinear planar CC of four bodies. Then there is a constant $\sigma<0$ such that
\begin{equation}\label{eq:dziobek}
m_im_j\,w_{ij}=\sigma\,A_iA_j\qquad\text{for all }i<j .
\end{equation}
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:nocollinear} no three bodies are collinear. By \eqref{eq:equil}, $(\omega_e)$ is a self-stress, so Lemma~\ref{lem:rigid} gives \eqref{eq:dziobek} for some $\sigma\in\R$. If $\sigma=0$, all six distances equal $\lambda'^{-1/3}$, which is impossible in the plane. Note that $w_e>0$ if and only if $r_e<\lambda'^{-1/3}$. Suppose $\sigma>0$. If $q$ is convex, then by Lemma~\ref{lem:areas}(d) $A_iA_j>0$ on the diagonals and $A_iA_j<0$ on the sides, so every diagonal is shorter than every side. But if the diagonals are $q_iq_k$ and $q_jq_l$ and meet at $p$, the triangle inequality gives
\[
r_{ik}+r_{jl}=|q_i-p|+|p-q_k|+|q_j-p|+|p-q_l|>r_{ij}+r_{kl},
\]
a contradiction. If $q$ is concave, say with $q_4$ inside the triangle $q_1q_2q_3$, then $A_iA_4<0<A_iA_j$ for $i,j\le3$. Every interior edge $q_iq_4$ would then be longer than every exterior edge. But writing $q_4=\alpha q_1+\beta q_2+\gamma q_3$ with $\alpha,\beta,\gamma>0$ and $\alpha+\beta+\gamma=1$, we get $r_{14}\le\beta r_{12}+\gamma r_{13}<\max(r_{12},r_{13})$, again a contradiction.
\end{proof}

\begin{proposition}\label{prop:convexsigns}
Let $q$ be a convex CC whose cyclic order is $(1234)$. Then:
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item $w_{12},w_{23},w_{34},w_{14}>0>w_{13},w_{24}$. Equivalently,
\[
\min(r_{13},r_{24})>\lambda'^{-1/3}>\max(r_{12},r_{23},r_{34},r_{14}),
\]
so each diagonal is longer than each side.
\item $w_{12}w_{34}=w_{13}w_{24}=w_{14}w_{23}$.
\item A longest side and a shortest side are opposite each other.
\end{enumerate}
\end{proposition}

\begin{proof}
(a) follows from \eqref{eq:dziobek}, $\sigma<0$, and the signs of $A_iA_j$. For (b), multiply the relations for complementary pairs of edges: $m_1m_2m_3m_4\,w_{12}w_{34}=\sigma^2A_1A_2A_3A_4$, and likewise for the other two pairings. For (c), suppose that $q_1q_2$ is a longest side. Since $w$ is a decreasing function of $r$, we have $0<w_{12}\le w_{14},w_{23}$. Then $w_{34}=w_{14}w_{23}/w_{12}\ge\max(w_{12},w_{14},w_{23})$, so $q_3q_4$ is a shortest side.
\end{proof}

These facts are classical; see \cite[Section~2.2]{CCR19} and the references there.

\section{An identity for the Hessian and a mass-free majorant}\label{sec:identity}

\subsection{The identity}

\begin{proposition}\label{prop:identity}
Let $q$ be a noncollinear planar CC of four bodies, and let $\sigma<0$ be as in Lemma~\ref{lem:dziobek}. Then
\begin{equation}\label{eq:identity}
Q(v)=K(v)-|\sigma|\,|L(v)|^2,\qquad L(v)=\sum_{l=1}^4A_lv_l\in\R^2 ,
\end{equation}
for all $v\in(\R^2)^4$.
\end{proposition}

\begin{proof}
By Lemma~\ref{lem:hessian}(a) and \eqref{eq:dziobek}, $Q(v)=K(v)-\sigma\sum_{i<j}A_iA_j|v_i-v_j|^2$. Expanding the squares and using $\sum_jA_j=0$,
\[
\sum_{i<j}A_iA_j|v_i-v_j|^2=\frac12\sum_{i,j}A_iA_j\bigl(|v_i|^2+|v_j|^2-2\ip{v_i}{v_j}\bigr)=-\Bigl|\sum_iA_iv_i\Bigr|^2 .
\]
Hence $Q=K+\sigma|L|^2=K-|\sigma||L|^2$.
\end{proof}

Since $K\ge0$ and $L$ takes values in $\R^2$, $Q$ is positive semidefinite on the kernel of $L$, which has codimension at most two. With Lemma~\ref{lem:shape} this gives the following bound, due to Palmore \cite{PalI,PalII}; see \cite[Proposition~21]{Moe15} and \cite[Proposition~5.7]{San26} for other proofs.

\begin{corollary}\label{cor:palmore}
Every noncollinear planar CC of four bodies has Morse index at most $2$.
\end{corollary}

\begin{remark}\label{rem:identity}
(i) Santoprete \cite{San26} works in pair space and decomposes the constrained Hessian as $H_C=L_\Delta+\widetilde L$. The gap Laplacian $L_\Delta$ is positive semidefinite, and the transverse part $\widetilde L$ has rank two for noncollinear four-body CCs. Proposition~\ref{prop:identity} is the analogous statement in the coordinates of the bodies: $K$ plays the role of $L_\Delta$, and $-|\sigma||L|^2$ is an explicit square that plays the role of $\widetilde L$, which Santoprete also writes in factored form \cite[Corollary~5.3]{San26}, with coefficients given by the Dziobek areas \cite[Remark~5.5]{San26}. Santoprete characterizes definiteness by an explicit $2\times2$ matrix. Proposition~\ref{prop:majorant}(c) below gives an analogous criterion with the matrix $G$.

(ii) In the language of rigidity theory, $\omega$ is a self-stress of the framework formed by the six edges, $\sum_e\omega_e|v_e|^2$ is its stress energy, and \eqref{eq:identity} says that the stress matrix of $\omega$ is the rank-one matrix $|\sigma|AA^{\mathsf T}$. The computation uses only that the self-stress is unique up to a factor and has product form. It therefore applies verbatim to Dziobek configurations of $d+2$ bodies in $\R^d$, where it gives $Q=K+\sigma|\sum_lA_lv_l|^2$ with $\sum_lA_lv_l\in\R^d$ and the $A_l$ the coefficients of the affine dependence.
\end{remark}

\subsection{Expressing \texorpdfstring{$L$}{L} through the edge variations}
The form $L$ vanishes on $\cT$: $\sum_lA_l=0$ kills translations and $\sum_lA_lJq_l=J\sum_lA_lq_l=0$ kills rotations. By Lemma~\ref{lem:rigid}, $L$ therefore factors through $\dr$. The next lemma gives an explicit factorization.

\begin{lemma}\label{lem:beta}
Suppose that no three of $q_1,\dots,q_4$ are collinear. For an edge $e=ij$ and an index $l\notin e$, let $k$ be the fourth index, so that $ijk$ is the triangle of the bodies other than $l$, and put $N_{e,l}=R_{ik}+R_{jk}-R_{ij}$. Define
\[
\beta_e=-\sum_{l\notin e}\frac{r_e\,N_{e,l}}{8A_l}\,q_l\ \in\R^2 .
\]
Then $L(v)=\sum_e\beta_e\,\dr_e(v)$ and $\sum_e\tau_e\,\dr_e(v)=0$ for all $v$. Consequently $L=\sum_e(\beta_e+\tau_ey)\,\dr_e$ for every $y\in\R^2$.
\end{lemma}

\begin{proof}
The identity $\sum_lA_l(q)\,q_l=0$ of Lemma~\ref{lem:areas}(a) holds for all $q$. Differentiating it in the direction $v$ gives $L(v)=-\sum_l dA_l(v)\,q_l$. Near $q$, $A_l$ is a smooth function of the side lengths of its triangle $ijk$. Heron's formula $16A_l^2=2(R_{ij}R_{ik}+R_{ij}R_{jk}+R_{ik}R_{jk})-R_{ij}^2-R_{ik}^2-R_{jk}^2$ gives $\partial A_l/\partial r_{ij}=r_{ij}N_{ij,l}/(8A_l)$, and similarly for the other two sides, with the sign of $A_l$ taken into account. Substituting $dA_l=\sum_{e\not\ni l}(\partial A_l/\partial r_e)\,\dr_e$ gives the first identity. The second is \eqref{eq:stressdual} applied to the self-stress $(A_iA_j)$.
\end{proof}

\subsection{The majorant}
Let $q$ be a noncollinear planar CC. For $e=ij$ put
\begin{equation}\label{eq:De}
D_e=-\frac{w_e}{3s_eA_iA_j} .
\end{equation}
By \eqref{eq:dziobek}, $\sigma=m_im_jw_e/(A_iA_j)$, and therefore $D_e=|\sigma|/\kappa_e>0$. For $y\in\R^2$ define the positive semidefinite $2\times2$ matrix
\[
S(y)=\sum_eD_e\,(\beta_e+\tau_ey)(\beta_e+\tau_ey)^{\mathsf T} .
\]
The quantities $D_e$, $\beta_e$ and $\tau_e$ are built from the configuration and from $\lambda'$. For a convex CC, Proposition~\ref{prop:convexsigns}(b) determines $\lambda'$ from the configuration:
\begin{equation}\label{eq:lambda}
\lambda'=\frac{s_{12}s_{34}-s_{13}s_{24}}{s_{12}+s_{34}-s_{13}-s_{24}},
\end{equation}
where the denominator is positive by Proposition~\ref{prop:convexsigns}(a). So on convex CCs, $S(y)$ is a function of the configuration alone, and the masses do not enter. Under $q\mapsto\mu q$ one has $D_e\mapsto|\mu|^{-4}D_e$, $\tau_e\mapsto|\mu|^5\tau_e$ and $\beta_e\mapsto|\mu|^2\frac{\mu}{|\mu|}\beta_e$. Hence the matrix $S(|\mu|^{-3}\frac{\mu}{|\mu|}y)$ of the configuration $\mu q$ is the matrix $S(y)$ of $q$ conjugated by a rotation. In particular the trace is unchanged.

\begin{proposition}\label{prop:majorant}
Let $q$ be a noncollinear planar CC of four bodies.
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item For all $v\in(\R^2)^4$ and $y\in\R^2$,
\[
|\sigma|\,|L(v)|^2\le\lmax(S(y))\,K(v)\le\tr S(y)\,K(v),\qquad\text{hence}\qquad Q\ge\bigl(1-\tr S(y)\bigr)K .
\]
\item Let $c_0=\sum_eD_e\tau_e^2>0$, $b_0=\sum_eD_e\tau_e\beta_e\in\R^2$, $y^*=-b_0/c_0$ and $G=S(y^*)=\sum_eD_e\beta_e\beta_e^{\mathsf T}-c_0^{-1}b_0b_0^{\mathsf T}$. Then
\[
S(y)=G+c_0\,(y-y^*)(y-y^*)^{\mathsf T},
\]
so $G\preceq S(y)$ for every $y$, and $\min_y\tr S(y)=\tr G$.
\item Let $\mu_1\ge\mu_2\ge0$ be the eigenvalues of $G$. The generalized eigenvalues of the pair $(Q,K)$ on the five-dimensional space $(\R^2)^4/\cT$ are $1,1,1,1-\mu_1,1-\mu_2$. In particular $Q\ge(1-\mu_1)K$ and the constant is optimal. The Morse index of $q$ is the number of $\mu_i>1$, and $q$ is degenerate if and only if $\mu_1=1$ or $\mu_2=1$.
\end{enumerate}
\end{proposition}

\begin{proof}
(a) Let $u\in\R^2$ be a unit vector. By Lemma~\ref{lem:beta} and the Cauchy--Schwarz inequality,
\[
\ip{u}{L(v)}^2=\Bigl(\sum_e\frac{\ip{u}{\beta_e+\tau_ey}}{\sqrt{\kappa_e}}\cdot\sqrt{\kappa_e}\,\dr_e(v)\Bigr)^2\le\Bigl(\sum_e\frac{\ip{u}{\beta_e+\tau_ey}^2}{\kappa_e}\Bigr)K(v).
\]
Multiplying by $|\sigma|$ and using $D_e=|\sigma|/\kappa_e$ gives $|\sigma|\ip{u}{L(v)}^2\le u^{\mathsf T}S(y)u\,K(v)$. Take the supremum over $u$, use $\lmax\le\tr$ for positive semidefinite matrices, and apply Proposition~\ref{prop:identity}.

(b) This is completing the square. We have $c_0>0$ because $\tau\ne0$.

(c) By Lemma~\ref{lem:rigid}, $\dr$ identifies $V=(\R^2)^4/\cT$ with the hyperplane $\tau^\perp\subset\R^6$. Under this identification $K$ becomes the restriction of $k(z)=\sum_e\kappa_ez_e^2$, and by Lemma~\ref{lem:beta} $L$ becomes $z\mapsto\sum_e\beta_ez_e$. For $g\in\R^6$,
\[
\sup_{0\ne z\in\tau^\perp}\frac{(\sum_eg_ez_e)^2}{k(z)}=\min_{t\in\R}\sum_e\frac{(g_e+t\tau_e)^2}{\kappa_e} .
\]
Indeed, $\sum_eg_ez_e=\sum_e(g_e+t\tau_e)z_e$ on $\tau^\perp$, so the Cauchy--Schwarz inequality gives ``$\le$''. Equality holds for $z_e=(g_e+t^*\tau_e)/\kappa_e$, where $t^*$ is the minimizer, because this $z$ lies in $\tau^\perp$. Taking $g_e=\ip{u}{\beta_e}$ and multiplying by $|\sigma|$ gives
\[
\sup_{v\notin\cT}\frac{|\sigma|\ip{u}{L(v)}^2}{K(v)}=\min_t\sum_eD_e\bigl(\ip{u}{\beta_e}+t\tau_e\bigr)^2=u^{\mathsf T}Gu\qquad(u\in\R^2).
\]
Let $\mathcal K:V\to V^*$ be the isomorphism defined by $K$. The last identity says $|\sigma|\,L\mathcal K^{-1}L^{\mathsf T}=G$. The generalized eigenvalues of $(Q,K)$ are the eigenvalues of $\mathcal K^{-1}Q=\mathrm{Id}-|\sigma|\mathcal K^{-1}L^{\mathsf T}L$. This operator is self-adjoint for $K$. The operator $|\sigma|\mathcal K^{-1}L^{\mathsf T}L$ on the five-dimensional space $V$ has rank at most two, and its characteristic polynomial is $t^3$ times that of $|\sigma|L\mathcal K^{-1}L^{\mathsf T}=G$. This gives the list of generalized eigenvalues. The remaining statements follow from Lemma~\ref{lem:shape}, because $Q$ vanishes on $\cT$.
\end{proof}

\begin{corollary}\label{cor:criterion}
Let $q$ be a noncollinear planar CC of four bodies. If $\tr S(y)<1$ for some $y\in\R^2$, then $Q\ge(1-\tr S(y))K$, and $q$ is a nondegenerate local minimum of $f_m$.
\end{corollary}

\begin{proof}
Combine Proposition~\ref{prop:majorant}(a), Lemma~\ref{lem:rigid} and Lemma~\ref{lem:shape}.
\end{proof}

\begin{remark}\label{rem:trace}
The sharp quantity is $\lmax(G)$, while the certificate below uses $\tr S(y)$, which satisfies $\tr S(y)\ge\tr G\ge\lmax(G)$. The trace is a sum of squares with explicit coefficients. It is well suited to interval arithmetic, and a single vector $y$ can serve for a whole box of configurations, so there is no need to locate $y^*$ exactly. The loss is moderate. Numerically, the supremum of $\tr G$ over convex CCs is about $0.5927$, approached at the boundary of the family of kites symmetric about the diagonal $q_1q_3$, where $q_1q_2q_4$ is equilateral and $m_3\to0$. The supremum of $\lmax(G)$ is at least $\frac13$, a limit value at the corner where two of the masses tend to zero (Proposition~\ref{prop:corner}). Numerically it equals $\frac13$ and is not attained (Figure~\ref{fig:lmax} in Section~\ref{sec:cap}). This suggests that the optimal constant in Theorem~B is $\frac23$ (Conjecture~\ref{conj:sharp}).
\end{remark}

\section{Normalized coordinates}\label{sec:normal}

\subsection{The coordinates of Corbera, Cors and Roberts}
Following \cite{CCR19}, for $a,b,c>0$ and $-1<x<1$ put $s=\sqrt{1-x^2}$ and let $q(a,b,c,x)$ be the configuration
\[
q_1=(1,0),\qquad q_2=a\,(x,s),\qquad q_3=(-b,0),\qquad q_4=-c\,(x,s).
\]
Its diagonals $q_1q_3$ and $q_2q_4$ meet at the origin, which is an interior point of both, and $q_2$ lies in the upper half-plane. Hence $q(a,b,c,x)$ is a strictly convex quadrilateral whose vertices $q_1,q_2,q_3,q_4$ are in counterclockwise order. Its squared mutual distances and oriented areas are
\begin{gather*}
R_{12}=1+a^2-2ax,\qquad R_{13}=(1+b)^2,\qquad R_{14}=1+c^2+2cx,\\
R_{23}=a^2+b^2+2abx,\qquad R_{24}=(a+c)^2,\qquad R_{34}=b^2+c^2-2bcx,\\
(A_1,A_2,A_3,A_4)=\tfrac{s}{2}\bigl(b(a+c),\,-c(1+b),\,a+c,\,-a(1+b)\bigr).
\end{gather*}
Consider the six functions
\begin{align*}
g_1&=b^2+2b-a^2+2ax, & g_2&=c^2+2ac-1+2ax, & g_3&=a-c-2x,\\
g_4&=1-b-2ax, & g_5&=a-c+2bx, & g_6&=1-b+2cx .
\end{align*}
Expanding the squared distances gives
\begin{equation}\label{eq:gfact}
\begin{gathered}
R_{13}-R_{12}=g_1,\qquad R_{24}-R_{12}=g_2,\qquad R_{12}-R_{14}=(a+c)\,g_3,\\
R_{12}-R_{23}=(1+b)\,g_4,\qquad R_{23}-R_{34}=(a+c)\,g_5,\qquad R_{14}-R_{34}=(1+b)\,g_6 .
\end{gathered}
\end{equation}
Let
\[
\cC=\bigl\{(a,b,c,x)\in(0,\infty)^3\times(-1,1):\ g_1>0,\ g_2>0,\ g_3\ge0,\ g_4\ge0,\ g_5\ge0,\ g_6\ge0\bigr\}.
\]
By \eqref{eq:gfact}, a point $(a,b,c,x)$ with $a,b,c>0$ lies in $\cC$ if and only if
\begin{equation}\label{eq:order}
r_{13}>r_{12},\quad r_{24}>r_{12},\quad r_{12}\ge r_{14}\ge r_{34},\quad r_{12}\ge r_{23}\ge r_{34}.
\end{equation}
In words, $q_1q_2$ is a longest side, $q_3q_4$ is a shortest side, and both diagonals are longer than $q_1q_2$. This is the normalization used in \cite[Section~3]{CCR19}.

\subsection{The Dziobek function}
For $X,Y>0$ let
\[
\psi(X,Y)=\frac{X+\sqrt{XY}+Y}{(\sqrt X+\sqrt Y)\,(XY)^{3/2}} ,
\]
a positive real-analytic function with $X^{-3/2}-Y^{-3/2}=(Y-X)\,\psi(X,Y)$ and $\psi(1,1)=\frac32$. For $(a,b,c,x)\in\cC$ we compare the numbers $s_e=R_e^{-3/2}$ with $s_{12}$:
\[
\eta_{13}=s_{12}-s_{13},\quad \eta_{24}=s_{12}-s_{24},\quad \eta_{14}=s_{14}-s_{12},\quad \eta_{23}=s_{23}-s_{12},\quad \eta_{34}=s_{34}-s_{12}.
\]
By \eqref{eq:gfact},
\begin{equation}\label{eq:etafact}
\begin{gathered}
\eta_{13}=g_1\,\psi(R_{12},R_{13}),\qquad \eta_{24}=g_2\,\psi(R_{12},R_{24}),\qquad \eta_{14}=(a+c)\,g_3\,\psi(R_{14},R_{12}),\\
\eta_{23}=(1+b)\,g_4\,\psi(R_{23},R_{12}),\qquad \eta_{34}=\bigl((1+b)\,g_4+(a+c)\,g_5\bigr)\,\psi(R_{34},R_{12}).
\end{gathered}
\end{equation}
In particular $\eta_{13},\eta_{24}>0$ and $\eta_{14},\eta_{23},\eta_{34}\ge0$ on $\cC$. Put
\[
\delta=\eta_{13}+\eta_{24}+\eta_{34}=s_{12}+s_{34}-s_{13}-s_{24}>0
\]
and define the \emph{Dziobek function}
\begin{equation}\label{eq:P}
P=\eta_{14}\eta_{23}\,\delta+\eta_{13}\eta_{24}\,(\eta_{14}+\eta_{23}-\eta_{34}) .
\end{equation}
The factored forms \eqref{eq:etafact} are the ones used in the computation. They make the signs of the $\eta_e$ visible and avoid cancellation near the boundary of $\cC$.

\begin{lemma}\label{lem:dziobekfn}
Let $(a,b,c,x)\in\cC$ and $q=q(a,b,c,x)$. Define $\lambda'$ by \eqref{eq:lambda}, that is, $\lambda'=(s_{12}s_{34}-s_{13}s_{24})/\delta$, and put $w_e=s_e-\lambda'$.
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item We have
\begin{gather*}
w_{12}=\frac{\eta_{13}\eta_{24}}{\delta},\qquad w_{34}=\frac{(\eta_{13}+\eta_{34})(\eta_{24}+\eta_{34})}{\delta},\qquad w_{13}=-\frac{\eta_{13}(\eta_{13}+\eta_{34})}{\delta},\\
w_{24}=-\frac{\eta_{24}(\eta_{24}+\eta_{34})}{\delta},\qquad w_{14}=\eta_{14}+w_{12},\qquad w_{23}=\eta_{23}+w_{12}.
\end{gather*}
Consequently $w_{12},w_{14},w_{23},w_{34}>0>w_{13},w_{24}$, $\;w_{12}w_{34}=w_{13}w_{24}$ and $w_{12}w_{34}-w_{14}w_{23}=-P/\delta$.
\item Let $F$ be the polynomial of \cite[Lemma~3.1]{CCR19},
\[
F=(r_{24}^3-r_{14}^3)(r_{13}^3-r_{12}^3)(r_{23}^3-r_{34}^3)-(r_{12}^3-r_{14}^3)(r_{24}^3-r_{34}^3)(r_{13}^3-r_{23}^3).
\]
Then $F\cdot\prod_es_e=-P$.
\item $q$ is a central configuration for some positive masses if and only if $P=0$. In that case the masses are unique up to a common positive factor. Normalizing $\sigma=-1$ in \eqref{eq:dziobek}, they are determined by $m_im_j=-A_iA_j/w_{ij}$ for all $i<j$.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) Since $\delta=s_{12}+s_{34}-s_{13}-s_{24}$, we get $\delta\,w_{12}=\delta s_{12}-s_{12}s_{34}+s_{13}s_{24}=(s_{12}-s_{13})(s_{12}-s_{24})=\eta_{13}\eta_{24}$. In the same way $\delta w_{34}=(s_{34}-s_{13})(s_{34}-s_{24})$ and $\delta w_{13}=(s_{12}-s_{13})(s_{13}-s_{34})$, $\delta w_{24}=(s_{12}-s_{24})(s_{24}-s_{34})$. Moreover $w_{14}-w_{12}=s_{14}-s_{12}$ and $w_{23}-w_{12}=s_{23}-s_{12}$. This proves the formulas, and the signs follow from the signs of the $\eta_e$. The identity $w_{12}w_{34}=w_{13}w_{24}$ is immediate from the formulas. Finally $w_{34}-w_{12}=\eta_{34}$, so
\[
w_{12}w_{34}-w_{14}w_{23}=w_{12}(\eta_{34}-\eta_{14}-\eta_{23})-\eta_{14}\eta_{23}=-P/\delta .
\]
(b) Writing $r_e^3=1/s_e$, each factor of $F$ becomes a difference of two $s_e$ divided by their product, and both products of three factors have denominator $\prod_es_e$. Hence
\[
F\prod_es_e=(s_{14}-s_{24})(s_{12}-s_{13})(s_{34}-s_{23})-(s_{14}-s_{12})(s_{34}-s_{24})(s_{23}-s_{13}).
\]
Substituting $s_{14}-s_{24}=\eta_{14}+\eta_{24}$, $s_{34}-s_{23}=\eta_{34}-\eta_{23}$, $s_{34}-s_{24}=\eta_{34}+\eta_{24}$, $s_{23}-s_{13}=\eta_{23}+\eta_{13}$ and expanding gives $-P$.

(c) Suppose that $q$ is a CC for positive masses. The relation $w_{12}w_{34}=w_{13}w_{24}$ of Proposition~\ref{prop:convexsigns}(b) is linear in $\lambda'$ and forces $\lambda'$ to be given by \eqref{eq:lambda}. So the $w_e$ of the CC are those of part (a), and $w_{12}w_{34}=w_{14}w_{23}$ gives $P=0$. By \eqref{eq:dziobek}, $m_im_j=\sigma A_iA_j/w_{ij}$, so the six products $m_im_j$, and hence the masses, are determined up to a common factor. Conversely, suppose $P=0$ and put $\mu_{ij}=-A_iA_j/w_{ij}$. By Lemma~\ref{lem:areas}(d), $A_iA_j<0$ on the sides and $A_iA_j>0$ on the diagonals, so part (a) gives $\mu_{ij}>0$ for all six edges. By part (a) and $P=0$, $\mu_{12}\mu_{34}=\mu_{13}\mu_{24}=\mu_{14}\mu_{23}$. Therefore $m_1=(\mu_{12}\mu_{13}/\mu_{23})^{1/2}$, $m_2=\mu_{12}/m_1$, $m_3=\mu_{13}/m_1$, $m_4=\mu_{14}/m_1$ are positive and satisfy $m_im_j=\mu_{ij}$ for all $i<j$. With these masses $\omega_{ij}=m_im_jw_{ij}=-A_iA_j$, which is a self-stress by Lemma~\ref{lem:rigid}. So \eqref{eq:equil} holds, and $q$ is a CC.
\end{proof}

Let
\[
\cE=\{(a,b,c,x)\in\cC:\ P(a,b,c,x)=0\}.
\]
By Lemma~\ref{lem:dziobekfn}(b), $\cE$ is the set denoted $E$ in \cite{CCR19}, defined there by $F=0$. Corbera, Cors and Roberts show that the points of $E$ are exactly the convex CCs, up to relabelling and similarity \cite[Lemma~3.1]{CCR19}. We record this in the form in which we use it.

\begin{lemma}\label{lem:normal}
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item For every $(a,b,c,x)\in\cE$, the configuration $q(a,b,c,x)$ is a counterclockwise convex CC with cyclic order $(1234)$ for positive masses, which are unique up to a common factor.
\item Let $q$ be a convex CC for positive masses $m_1,\dots,m_4$. Then there are a permutation $\pi$ of $\{1,2,3,4\}$, a similarity $T$ of the plane and a point $(a,b,c,x)\in\cE$ such that the configuration $q'$ defined by $q'_{\pi(i)}=T(q_i)$ equals $q(a,b,c,x)$. It is a CC for the masses $m'$ defined by $m'_{\pi(i)}=m_i$.
\item The map $\cE\to\cS$, $(a,b,c,x)\mapsto[q(a,b,c,x)]$, is injective.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) is Lemma~\ref{lem:dziobekfn}(c). (b) Label the bodies so that the cyclic order is $(1234)$ and $q_1q_2$ is a longest side. By Proposition~\ref{prop:convexsigns}, $q_3q_4$ is a shortest side and both diagonals are longer than every side, so \eqref{eq:order} holds. These relations are preserved by similarities. If the vertices are in clockwise order, apply a reflection. Then apply the orientation-preserving similarity that moves the intersection point of the diagonals to the origin and $q_1$ to $(1,0)$. Now $q_3=(-b,0)$ with $b>0$, and $q_2=a(\cos\theta,\sin\theta)$, $q_4=-c(\cos\theta,\sin\theta)$ with $a,c>0$. Since the order is counterclockwise, $0<\theta<\pi$. So the configuration is $q(a,b,c,\cos\theta)$, and $(a,b,c,\cos\theta)\in\cC$ by \eqref{eq:order}. It is a CC because the equations \eqref{eq:cc} are invariant under similarities and under a simultaneous permutation of bodies and masses. Lemma~\ref{lem:dziobekfn}(c) gives $P=0$.
(c) If $q(a',b',c',x')=\mu\,q(a,b,c,x)+t\mathbb 1$ with $\mu\in\C^*$ and $t\in\C$, the similarity maps the intersection point of the diagonals to itself, so $t=0$. It fixes $q_1=(1,0)$, so $\mu=1$.
\end{proof}

\begin{remark}\label{rem:involution}
The normal form is not unique. In the proof of (b), the two endpoints of a longest side can be labelled in either order. Exchanging the labels $1\leftrightarrow2$ and $3\leftrightarrow4$, reflecting, and renormalizing maps $(a,b,c,x)$ to $(1/a,c/a,b/a,x)$. This map preserves $\cE$ and permutes the masses as $(m_1,m_2,m_3,m_4)\mapsto(m_2,m_1,m_4,m_3)$. So an unlabelled similarity class of convex CCs can appear more than once in $\cE$. This does not matter for the estimate of $\tr S$, which is a property of each point of $\cE$.
\end{remark}

\subsection{A priori bounds}

\begin{lemma}[{\cite[Lemma~3.2]{CCR19}}]\label{lem:bounds}
On $\cC$,
\[
c\le a,\qquad b\le1,\qquad ac<b^2+2b,\qquad a^2<b^2+b+1,\qquad a^2+ac+c^2>1 .
\]
Consequently $\frac1{\sqrt3}<a<\sqrt3$, $0<c\le a$ and $0<b\le1$.
\end{lemma}

\begin{proof}
If $x\ge0$ then $g_3\ge0$ gives $a-c\ge2x\ge0$, and $g_4\ge0$ gives $1-b\ge2ax\ge0$. If $x<0$ then $g_5\ge0$ gives $a-c\ge-2bx>0$, and $g_6\ge0$ gives $1-b\ge-2cx>0$. The remaining inequalities are $g_1+a\,g_3=b^2+2b-ac>0$, $g_1+g_4=b^2+b+1-a^2>0$ and $g_2+a\,g_3=c^2+ac+a^2-1>0$. Finally $a^2<b^2+b+1\le3$, and $1<a^2+ac+c^2\le3a^2$.
\end{proof}

Hence the projection of $\cE\cap\{b\ge\frac18\}$ to $(a,b,c)$ is contained in the box
\[
\Omega_{\mathrm{dir}}=[\tfrac12,\tfrac74]\times[\tfrac18,1]\times[0,\tfrac74].
\]

\subsection{The blow-up chart}\label{sec:chart}
As $b\to0$ on $\cE$, Lemma~\ref{lem:bounds} forces $c\to0$ (because $ac<b^2+2b$ and $a>1/\sqrt3$), and $a\to1$, $x\to\frac12$ by Lemma~\ref{lem:chartbounds} and the bounds on $\xi$ below. So the configuration degenerates to $q_1=(1,0)$, $q_2=(\frac12,\frac{\sqrt3}2)$, $q_3=q_4=0$: the bodies $3$ and $4$ collide at a point that forms an equilateral triangle with $q_1$ and $q_2$. To resolve this corner we use the coordinates $(b,\alpha,\gamma,\xi)$ defined by
\[
a=1+b\alpha,\qquad c=b\gamma,\qquad x=\tfrac12+b\xi .
\]

\begin{lemma}\label{lem:chartbounds}
Let $(a,b,c,x)\in\cC$ with $0<b\le\frac18$. Then
\[
-2<\alpha<\frac{1+b}{2}\le\frac9{16},\qquad 0<\gamma<\frac{2+b}{1-2b}\le\frac{17}{6}.
\]
In particular $a>1-2b\ge\frac34$.
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:bounds}, $a^2<1+b+b^2$, so $a<1+\frac12(b+b^2)$ and $\alpha<\frac12(1+b)$.

For the lower bound put $u=b^2+2b\le\frac{17}{64}<\frac13$. Lemma~\ref{lem:bounds} gives $c<u/a$ and $1<a^2+ac+c^2$. Since $c\mapsto ac+c^2$ is increasing for $c>0$, we get $1<a^2+u+u^2/a^2$, that is, $p(a^2)>0$, where
\[
p(t)=t^2-(1-u)\,t+u^2 .
\]
The roots of $p$ are $t_\pm=\frac12\bigl(1-u\pm\sqrt{(1-3u)(1+u)}\bigr)$, which are real. Since $p(\frac13)=(u+\frac23)(u-\frac13)<0$, we have $t_-<\frac13<t_+$. As $a^2>\frac13$ and $p(a^2)>0$, it follows that $a^2>t_+$. Next, $p(t)=t\,(f(t)-1)$ with $f(t)=t+u+u^2/t$, and a direct computation gives
\[
f\bigl((1-2b)^2\bigr)-1=\frac{b\,(7b-1)\,(3b^2-3b+2)}{(1-2b)^2}<0\qquad(0<b<\tfrac17).
\]
Hence $p((1-2b)^2)<0$, so $(1-2b)^2<t_+<a^2$. This gives $a>1-2b$, that is, $\alpha>-2$.

Finally $c<u/a<u/(1-2b)$, so $\gamma=c/b<(2+b)/(1-2b)$.
\end{proof}

So the projection of $\cE\cap\{0<b\le\frac18\}$ to $(b,\alpha,\gamma)$ is contained in
\[
\Omega_{\mathrm{ch}}=[0,\tfrac18]\times[-2,1]\times[0,3].
\]
We now rewrite all quantities in the chart; the complete list is in \hyperref[app:chart]{the Appendix}. The functions $g_1,\dots,g_4$ are divisible by $b$, and we put $h_i=g_i/b$ for $i\le4$ and $h_i=g_i$ for $i=5,6$:
\begin{align*}
h_1&=2-\alpha+2\xi+b\,(1-\alpha^2+2\alpha\xi), & h_2&=2\gamma+2\xi+\alpha+b\,(\gamma^2+2\alpha\gamma+2\alpha\xi),\\
h_3&=\alpha-\gamma-2\xi, & h_4&=-(1+\alpha+2\xi+2b\alpha\xi),\\
h_5&=1+b\,(\alpha-\gamma+1+2b\xi), & h_6&=1-b+b\gamma+2b^2\gamma\xi .
\end{align*}
The squared lengths are $R_e=1+b\,d_e$ for $e\ne34$ and $R_{34}=b^2\rho^2$, where
\begin{gather*}
d_{12}=\alpha-2\xi+b(\alpha^2-2\alpha\xi),\qquad d_{13}=2+b,\qquad d_{14}=\gamma(b\gamma+2x),\\
d_{23}=2\alpha+b\alpha^2+2x(1+b\alpha)+b,\qquad d_{24}=2(\alpha+\gamma)+b(\alpha+\gamma)^2,\qquad \rho^2=1-2\gamma x+\gamma^2 .
\end{gather*}
The gaps $\eta_e$ are rescaled as
\begin{gather*}
\hat\eta_{13}=\frac{\eta_{13}}b=h_1\psi(R_{12},R_{13}),\qquad \hat\eta_{24}=\frac{\eta_{24}}b=h_2\psi(R_{12},R_{24}),\\
\hat\eta_{14}=\frac{\eta_{14}}b=(a+c)\,h_3\,\psi(R_{14},R_{12}),\qquad \hat\eta_{23}=\frac{\eta_{23}}b=(1+b)\,h_4\,\psi(R_{23},R_{12}),\\
\hat\eta_{34}=b^3\eta_{34}=\rho^{-3}-b^3s_{12},\qquad \hat\delta=b^3\delta=\hat\eta_{34}+b^4(\hat\eta_{13}+\hat\eta_{24}),
\end{gather*}
and then
\begin{equation}\label{eq:Phat}
\hat P=b\,P=\hat\eta_{14}\hat\eta_{23}\,\hat\delta+\hat\eta_{13}\hat\eta_{24}\bigl(b^4(\hat\eta_{14}+\hat\eta_{23})-\hat\eta_{34}\bigr).
\end{equation}
In the chart, $\alpha$, $\gamma$ and $b$ are the independent coordinates, and $\xi$ plays the role of $x$. The inequalities $h_1,h_2>0$ and $h_3,h_4\ge0$ are linear in $\xi$, with coefficients $2a$, $2a$, $-2$ and $-2a$ in front of $\xi$, where $a>0$. So they confine $\xi$ to an explicit bounded interval (Section~\ref{sec:cap}).

The areas scale as $A_1=b\hA_1$ and $A_2=b\hA_2$, with $\hA_1=\frac s2(a+c)$ and $\hA_2=-\frac s2\gamma(1+b)$, while $A_3$ and $A_4$ are unchanged. The quantities $w_e$ scale as $w_{12}=b^5\hw_{12}$, $w_e=b\,\hw_e$ for $e\in\{13,14,23,24\}$ and $w_{34}=b^{-3}\hw_{34}$. Inserting these into the definitions of $D_e$ and $\beta_e$, all negative powers of $b$ cancel, and every $\tau_e$ is divisible by $b$. We put $T_e=\tau_e/b$ and
\[
\widehat S(Y)=\sum_eD_e\,(\beta_e+T_eY)(\beta_e+T_eY)^{\mathsf T},\qquad\text{so that}\qquad \widehat S(Y)=S(Y/b)\quad(b>0).
\]
\hyperref[app:chart]{The Appendix} gives $D_e$, $T_e$ and $\beta_e$ as explicit expressions in $(b,\alpha,\gamma,\xi)$, built from $h_i$, $d_e$, $\rho$, $s$, $\psi$ and the $\hat\eta_e$ by rational operations and square roots. These expressions are real-analytic wherever the square roots have positive arguments and the denominators do not vanish, in particular at points with $b=0$ and $\gamma>0$.

\begin{lemma}\label{lem:bzero}
At $b=0$ we have $x=\frac12$, $\rho^2=\gamma^2-\gamma+1$, and
\[
\hat P(0,\alpha,\gamma,\xi)=-\frac94\,\rho^{-3}\bigl(3\alpha+3\gamma-3\alpha\gamma+2(1+\gamma)\xi\bigr),\qquad
\frac{\partial\hat P}{\partial\xi}(0,\alpha,\gamma,\xi)=-\frac92\,(1+\gamma)\,\rho^{-3}<0 .
\]
Hence, near every point of $\{b=0,\ \gamma>0\}$ where $\hat P=0$, the zero set of $\hat P$ is the graph of a real-analytic function $\xi(b,\alpha,\gamma)$ with $\xi(0,\alpha,\gamma)=\frac{3(\alpha\gamma-\alpha-\gamma)}{2(1+\gamma)}$.
\end{lemma}

\begin{proof}
At $b=0$, $R_e=1$ for $e\ne34$, so every $\psi$ equals $\frac32$, $a+c=1+b=1$ and $\hat\delta=\hat\eta_{34}=\rho^{-3}$. Thus $\hat P=\frac94\rho^{-3}(h_3h_4-h_1h_2)$ with $h_1=2-\alpha+2\xi$, $h_2=2\gamma+\alpha+2\xi$, $h_3=\alpha-\gamma-2\xi$ and $h_4=-(1+\alpha+2\xi)$. Expanding, the terms quadratic in $\xi$ cancel, and $h_3h_4-h_1h_2=-(3\alpha+3\gamma-3\alpha\gamma+2(1+\gamma)\xi)$. The last statement is the analytic implicit function theorem.
\end{proof}

So in the chart the closure of $\cE$ is, near $b=0$, an analytic graph over $(b,\alpha,\gamma)$ that crosses $b=0$ transversally. This is why a uniform estimate can hold up to the corner.

\begin{remark}\label{rem:corner}
Near the corner the masses degenerate. By Lemma~\ref{lem:dziobekfn}(c), $m_1m_2=-A_1A_2/w_{12}$ is of order $b^{-3}$, $m_3m_4=-A_3A_4/w_{34}$ is of order $b^{3}$, and the other four products are of order $1$. Hence $m_3/m_1$ and $m_4/m_2$ are of order $b^3$. For example, along $\alpha=-\frac12$, $\gamma=\frac65$ one finds $m_3/m_1\approx0.1506\,b^3$ and $m_4/m_2\approx2.197\,b^3$ as $b\to0$ (Proposition~\ref{prop:corner}(b)). This end of $\cE$ is thus the regime of two small masses near an equilateral Lagrangian point of the two large ones.
\end{remark}

\section{The computer-assisted part}\label{sec:cap}

This section proves the following estimate.

\begin{proposition}\label{prop:cap}
Let $(a,b,c,x)\in\cE$, and let $S$ and $\widehat S$ be the matrices of Sections~\ref{sec:identity} and~\ref{sec:chart} for the configuration $q(a,b,c,x)$.
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item If $b\ge\frac18$, there is $y\in\R^2$ with $\tr S(y)<\frac34$.
\item If $0<b\le\frac18$, there is $Y\in\R^2$ with $\tr\widehat S(Y)<\frac34$.
\end{enumerate}
Consequently $\lmax(G)\le\tr G<\frac34$ at every point of $\cE$.
\end{proposition}

The last statement follows from (a) and (b), because $\widehat S(Y)=S(Y/b)$ and $\tr G=\min_y\tr S(y)$ by Proposition~\ref{prop:majorant}(b). Part (a) concerns a compact region, and part (b) the end of $\cE$ at the corner $b=0$. Both are proved by a rigorous computation, which we now describe. The programs, the certificate files and the logs are available; see the statement on data and code availability at the end of the paper.

\subsection{What is computed}\label{sec:what}
There are two computations. Each uses three independent coordinates $p$ and one dependent coordinate.
\begin{itemize}[leftmargin=2em]
\item \emph{Direct:} $p=(a,b,c)\in\Omega_{\mathrm{dir}}$, and the dependent coordinate is $x$. The functions are $g_1,\dots,g_6$, the Dziobek function $P$, and $t_y=\tr S(y)=\sum_eD_e\,|\beta_e+\tau_ey|^2$ for $y\in\R^2$.
\item \emph{Chart:} $p=(b,\alpha,\gamma)\in\Omega_{\mathrm{ch}}$, and the dependent coordinate is $\xi$. The functions are $h_1,\dots,h_6$, $\hat P$, and $t_Y=\tr\widehat S(Y)=\sum_eD_e\,|\beta_e+T_eY|^2$ for $Y\in\R^2$.
\end{itemize}
In the direct computation, $P$ is evaluated by \eqref{eq:P} with the factored forms \eqref{eq:etafact}, where $\psi(X,Y)=(X+\sqrt X\sqrt Y+Y)/\bigl((\sqrt X+\sqrt Y)\,X\sqrt X\,Y\sqrt Y\bigr)$. The quantities $D_e$, $\tau_e$ and $\beta_e$ are evaluated from their definitions \eqref{eq:De}, Lemma~\ref{lem:rigid} and Lemma~\ref{lem:beta}, with the $w_e$ of Lemma~\ref{lem:dziobekfn}(a). At a point of $\cE$ these $w_e$ are those of the central configuration $q(a,b,c,x)$, by the proof of Lemma~\ref{lem:dziobekfn}(c), so $t_y$ is the trace of the matrix $S(y)$ of that configuration. In the chart, all quantities are evaluated by the formulas of \hyperref[app:chart]{the Appendix}, and at points with $b>0$ they satisfy
\[
h_i=g_i/b\ (i\le4),\qquad h_i=g_i\ (i=5,6),\qquad \hat P=bP,\qquad t_Y=t_{Y/b}.
\]
In both computations, every function is obtained from the four coordinates by a finite sequence of additions, subtractions, multiplications, divisions, integer powers and square roots.

\begin{lemma}\label{lem:xrange}
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item Let $(a,b,c,x)\in\cC$. Then $\ell\le x\le u$, where
\[
\ell=\max\Bigl\{\frac{a^2-b^2-2b}{2a},\ \frac{1-c^2-2ac}{2a},\ \frac{c-a}{2b},\ \frac{b-1}{2c}\Bigr\},\qquad u=\min\Bigl\{\frac{a-c}{2},\ \frac{1-b}{2a}\Bigr\}.
\]
\item Let $(a,b,c,x)\in\cC$ with $0<b\le\frac18$, and let $(b,\alpha,\gamma,\xi)$ be its chart coordinates. Then $\hat\ell\le\xi\le\hat u$, where $a=1+b\alpha$ and
\[
\hat\ell=\max\Bigl\{\frac{\alpha-2-b(1-\alpha^2)}{2a},\ -\frac{2\gamma+\alpha+b(\gamma^2+2\alpha\gamma)}{2a}\Bigr\},\qquad \hat u=\min\Bigl\{-\frac{1+\alpha}{2a},\ \frac{\alpha-\gamma}{2}\Bigr\}.
\]
\end{enumerate}
\end{lemma}

\begin{proof}
(a) Solve $g_1>0$, $g_2>0$, $g_5\ge0$, $g_6\ge0$, $g_3\ge0$ and $g_4\ge0$ for $x$, using $a,b,c>0$. (b) Write $h_1=2-\alpha+b(1-\alpha^2)+2a\xi$, $h_2=2\gamma+\alpha+b(\gamma^2+2\alpha\gamma)+2a\xi$ and $h_4=-(1+\alpha+2a\xi)$. Since $b>0$, the conditions $g_1>0$, $g_2>0$, $g_4\ge0$ and $g_3\ge0$ are equivalent to $h_1>0$, $h_2>0$, $h_4\ge0$ and $h_3=\alpha-\gamma-2\xi\ge0$. Solve these for $\xi$, using $a>0$.
\end{proof}

\subsection{Ball arithmetic and mean-value enclosures}\label{sec:balls}
We use the ball arithmetic library Arb \cite{Joh17}, through its Python interface \texttt{python-flint}, at a working precision of $64$ bits. A ball is an interval $[m-r,m+r]$ with binary floating-point numbers $m$ and $r\ge0$. Every arithmetic operation, integer power and square root returns a ball that contains the exact results for all points of the input balls. In the version used (\texttt{python-flint} 0.9.0) the following holds, as we checked directly. The square root of a ball that is not contained in $(0,\infty)$ is NaN, except for the exact ball $0$, whose square root is $0$. A quotient by a ball that contains $0$ is NaN. Any arithmetic operation with a NaN operand, including multiplication by the exact $0$, returns NaN. Every comparison involving NaN is false, and so is every comparison involving a ball of infinite radius. Here a comparison such as $V<0$ means that every point of the ball $V$ is negative. We regard NaN as a ball that contains every real number; a NaN result is then a valid but useless enclosure. For interval methods in general see \cite{MKC09,Tuc11}.

We evaluate each function together with its gradient by forward-mode automatic differentiation over balls. The four coordinates are replaced by the four sides $Z_1,\dots,Z_4$ of a box $Z$, with the unit vectors as gradients. The rules are $(u\pm v)'=u'\pm v'$, $(uv)'=u\,v'+v\,u'$, $(u/v)'=(u'-(u/v)\,v')/v$, $(u^n)'=n\,u^{n-1}u'$ and $(\sqrt u)'=u'/(2\sqrt u)$, applied to each of the four components in ball arithmetic. The result is a ball $V$ and four balls $d_1,\dots,d_4$. We call this the \emph{jet evaluation} of the function on $Z$.

\begin{lemma}\label{lem:enclosure}
Let $f$ be given by a finite sequence of the operations above, in which every intermediate result is used, let $Z=\prod_i[\underline z_i,\overline z_i]$ be a box, and let $(V;d_1,\dots,d_4)$ be the jet evaluation of $f$ on $Z$.
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item Suppose that at least one of the balls $d_i$ is not NaN. Then, in the evaluation on $Z$, every square root has an argument ball contained in $(0,\infty)$ and every divisor ball excludes $0$. Consequently $f$ is real-analytic on a neighbourhood of $Z$, and $f(z)\in V$ and $\partial_if(z)\in d_i$ for all $z\in Z$ and all $i$.
\item Under the assumption of (a), let $\bar z\in Z$, let $r_i\ge\max(\overline z_i-\bar z_i,\ \bar z_i-\underline z_i)$, and let $F_{\bar z}$ be the ball evaluation of $f$ at $\bar z$. Then
\[
f(z)\in V\cap\Bigl(F_{\bar z}+\sum_{i=1}^4d_i\,[-r_i,r_i]\Bigr)\qquad\text{for all }z\in Z .
\]
\end{enumerate}
\end{lemma}

The program computes the intersection on the right of (b) with the intersection operation of Arb; we call the result the \emph{mean-value enclosure} of $f$ on $Z$. If the $d_i$ are NaN, the second ball is NaN, and so is the mean-value enclosure, because the intersection of a ball with NaN is NaN. Under the assumption of (a) the two balls intersect, by (b). (Should Arb report an empty intersection, the program would use the second ball alone, which by (b) is also an enclosure; this case does not occur.)

\begin{proof}
(a) Suppose that a square root in the evaluation has an argument ball $u$ that is not contained in $(0,\infty)$. If $u$ contains $0$, then $\sqrt u$ is NaN or, by the inclusion property, a ball that contains $0$. If $u$ is negative, $\sqrt u$ is NaN. In either case every component of the gradient $u'/(2\sqrt u)$ is NaN. The same holds for a quotient by a ball that contains $0$, because then the quotient and its gradient are NaN. By the differentiation rules and the NaN rules, if one operand of an operation has all four gradient components NaN, then so does the result. For the product rule this uses that $0\cdot\mathrm{NaN}$ is NaN. Since $f$ depends on every intermediate result, all four components of its gradient are then NaN, contrary to the assumption. This proves the first statement. So for every $z\in Z$, the exact evaluation of $f$ at $z$ takes square roots of positive numbers and divides by nonzero numbers, since these numbers lie in the corresponding balls. By compactness the same holds on a neighbourhood of $Z$, where $f$ is therefore real-analytic. The inclusion property of ball arithmetic, applied to the evaluation and to the chain rule, gives $f(z)\in V$ and $\partial_if(z)\in d_i$.

(b) By the mean value theorem, $f(z)=f(\bar z)+\sum_i\partial_if(\zeta)(z_i-\bar z_i)$ for some $\zeta$ on the segment from $\bar z$ to $z$, which lies in $Z$. Here $f(\bar z)\in F_{\bar z}$, $\partial_if(\zeta)\in d_i$ and $|z_i-\bar z_i|\le r_i$. Together with (a) this gives the claim.
\end{proof}

\subsection{The procedure}\label{sec:procedure}
Fix one of the two computations, and let $\Omega$ be its region. We divide $\Omega$ into an initial grid: $40\times28\times56$ cubes of side $\frac1{32}$ for $\Omega_{\mathrm{dir}}$, and $8\times96\times96$ boxes of sides $\frac1{64}\times\frac1{32}\times\frac1{32}$ for $\Omega_{\mathrm{ch}}$. All breakpoints are dyadic rationals and hence exact floating-point numbers. Each initial box is processed independently, as follows. For a box $B$ in $p$-space and an interval $X$ of the dependent coordinate, all enclosures below are taken on the box $B\times X$, with its floating-point midpoint $(\bar p,\bar x)$ and radii $r_i$ rounded upward. We write $w(B)$ for the largest side of $B$.

\begin{enumerate}[label=\textup{\arabic*.},leftmargin=2em]
\item \emph{Range.} Evaluate the bounds of Lemma~\ref{lem:xrange} in ball arithmetic on $B$, and round outward to an interval $X_0(B)$ of floating-point numbers: its lower end is the largest of the lower ends of the balls for the terms of $\ell$ (of $\hat\ell$), and its upper end is the smallest of the upper ends of the balls for the terms of $u$ (of $\hat u$). The denominators $2a$ and $2b$ are bounded away from $0$ on $\Omega_{\mathrm{dir}}$, and $a=1+b\alpha\ge\frac34$ on $\Omega_{\mathrm{ch}}$. The term $(b-1)/(2c)$ is used only if $c>0$ on $B$; omitting a term of $\ell$ only weakens the bound. In the direct computation $X_0(B)$ is intersected with $[-1,1]$. If $X_0(B)$ is empty, $B$ is \emph{discarded}.
\item \emph{Localization.} Starting from the list $\{X_0(B)\}$, process the intervals $X$ of the list one at a time.
\begin{enumerate}[label=(\roman*),leftmargin=1.8em]
\item If the mean-value enclosure of some $g_i$ (of some $h_i$ in the chart) is negative, drop $X$.
\item If the mean-value enclosure of $P$ (of $\hat P$ in the chart) is positive or negative, drop $X$.
\item Let $d_1,\dots,d_4$ be the derivative balls of $P$ (of $\hat P$), and suppose that $d_4$ is positive or negative. Put
\[
N=\bar x-\Bigl(F_{(\bar p,\bar x)}+\sum_{i=1}^3d_i\,[-r_i,r_i]\Bigr)\Big/d_4 ,
\]
where $F_{(\bar p,\bar x)}$ is the ball evaluation of $P$ at the midpoint. Replace $X$ by the outward rounding of $X\cap N$, and drop it if this is empty. If $N$ is NaN, $X$ is left unchanged. If the width of $X$ decreased by at least $30\%$, return to (i).
\item If the width of $X$ exceeds $\max(\frac14w(B),10^{-13})$, bisect $X$ at its floating-point midpoint and put both halves in the list. Otherwise keep $X$.
\end{enumerate}
When the list is empty, merge the kept intervals into maximal intervals, the \emph{runs} of $B$. If there are none, $B$ is \emph{discarded}.
\item \emph{Certification.} For each run $X$, compute in floating point the minimizer $y^*$ of $t_y$ (of $t_Y$) at the midpoint of $B\times X$, and let $y$ be the resulting pair of floating-point numbers. Compute the mean-value enclosure of $t_y$ on $B\times X$. The run is \emph{certified} if this enclosure is finite and its upper end, rounded up to a floating-point number $t_{B,X}$, is less than $\frac34$. If every run of $B$ is certified, $B$ is \emph{accepted}, and its runs, their vectors $y$ and their bounds $t_{B,X}$ are recorded.
\item \emph{Subdivision.} Otherwise bisect $B$ at the floating-point midpoint of one of its sides and process both halves. The side is chosen by a heuristic from the sizes of the terms $|d_i|\,r_i$ of the enclosure of $t_y$. The choice affects only the efficiency. The computation \emph{fails} if a box of width $w(B)<10^{-5}$ ($10^{-6}$ in the chart) would have to be bisected, or if an initial box produces more than $400000$ leaves.
\end{enumerate}
The processing of each initial box is deterministic, and any runtime error aborts the whole computation. The output is a certificate file, which lists for every initial box the bisection paths of its leaves, marks each leaf as accepted or discarded, and gives the runs, vectors $y$ and bounds $t_{B,X}$ of the accepted leaves.

\subsection{Correctness}\label{sec:correct}

\begin{lemma}\label{lem:soundness}
Suppose that the direct computation terminates without failure. Let $(a,b,c,x)\in\cE$ with $b\ge\frac18$. Then there are an accepted leaf $B\ni(a,b,c)$ and a run $X\ni x$ of $B$ such that the recorded $y$ and $t_{B,X}$ satisfy $\tr S(y)\le t_{B,X}<\frac34$ at $q(a,b,c,x)$. Likewise, suppose that the chart computation terminates without failure, and let $(a,b,c,x)\in\cE$ with $0<b\le\frac18$ and chart coordinates $(b,\alpha,\gamma,\xi)$. Then there are an accepted leaf $B\ni(b,\alpha,\gamma)$ and a run $X\ni\xi$ of $B$ such that the recorded $Y$ satisfies $\tr\widehat S(Y)\le t_{B,X}<\frac34$.
\end{lemma}

\begin{proof}
We give the proof for the direct computation and then list the changes for the chart. Let $z=(p,x)\in\cE$ with $p=(a,b,c)$ and $b\ge\frac18$.

\emph{Step 1: $p$ lies in a leaf.} By Lemma~\ref{lem:bounds}, $p\in\Omega_{\mathrm{dir}}$. The initial boxes are closed and cover $\Omega_{\mathrm{dir}}$. Bisecting a box at a floating-point number $m$ replaces a side $[\underline z,\overline z]$ by $[\underline z,m]$ and $[m,\overline z]$, so the two closed halves cover the box. Since the computation did not fail, every box was eventually accepted or discarded. Hence $p$ lies in a leaf $B$, accepted or discarded.

\emph{Step 2: $x$ survives the localization.} Since $z\in\cC$, Lemma~\ref{lem:xrange}(a) and outward rounding give $x\in X_0(B)$. We claim that during step~2 of the procedure, $x$ always lies in an interval of the list or in a kept interval. Suppose that $x\in X$ for an interval $X$ being processed. In (i), $g_i(z)\ge0$ for all $i$ because $z\in\cC$. The $g_i$ are polynomials, so Lemma~\ref{lem:enclosure} applies, and the enclosure of $g_i$ contains $g_i(z)$. So $X$ is not dropped. In (ii), an enclosure that is positive or negative is finite, so its derivative balls are not NaN, and by Lemma~\ref{lem:enclosure} it contains $P(z)=0$. Hence $X$ is not dropped. In (iii), $d_4$ is not NaN, so by Lemma~\ref{lem:enclosure}(a) the function $P$ is analytic near $B\times X$ and $\partial_iP\in d_i$ there. The mean value theorem in $p$, at the fixed value $\bar x\in X$, gives $P(p,\bar x)\in\Pi:=F_{(\bar p,\bar x)}+\sum_{i\le3}d_i[-r_i,r_i]$. The mean value theorem in the last variable gives $0=P(p,x)=P(p,\bar x)+\partial_xP(p,\zeta)\,(x-\bar x)$ for some $\zeta\in X$. Since $\partial_xP(p,\zeta)\in d_4$ and $0\notin d_4$, we get $x=\bar x-P(p,\bar x)/\partial_xP(p,\zeta)\in\bar x-\Pi/d_4=N$. So $x$ lies in the new interval $X\cap N$, and in particular this interval is not empty. In (iv), the two halves of $X$ cover $X$. This proves the claim. Since the list is eventually empty, $x$ lies in a kept interval, hence in a run $X$ of $B$. In particular $B$ is not discarded.

\emph{Step 3: the bound.} So $B$ was accepted, and the run $X\ni x$ was certified with the recorded $y$. The certified enclosure is finite, so its derivative balls are not NaN, and Lemma~\ref{lem:enclosure}(b) gives $t_y(z)\le t_{B,X}<\frac34$. By Section~\ref{sec:what}, $t_y(z)=\tr S(y)$ at $q(a,b,c,x)$.

\emph{The chart.} Now let $z=(b,\alpha,\gamma,\xi)$ with $0<b\le\frac18$, and put $p=(b,\alpha,\gamma)$. By Lemma~\ref{lem:chartbounds}, $p\in\Omega_{\mathrm{ch}}$. Lemma~\ref{lem:xrange}(b) gives $\xi\in X_0(B)$. Since $b>0$, we have $h_i(z)\ge0$ for all $i$, $\hat P(z)=bP(z)=0$ and $t_Y(z)=\tr\widehat S(Y)$. The rest of the argument is unchanged.
\end{proof}

Floating-point arithmetic enters only in the choice of the grid, the midpoints, the radii (which are rounded upward), the vectors $y$, the tolerance in (iv) and the bisections, and in the recorded bounds (which are rounded upward). None of these choices affects the argument.

\begin{proof}[Proof of Proposition~\ref{prop:cap}]
Both computations terminated without failure (Table~\ref{tab:runs}). Lemma~\ref{lem:soundness} gives (a) and (b).
\end{proof}

\subsection{Results}\label{sec:results}
Table~\ref{tab:runs} summarizes the two computations, which were run with $32$ processes on a machine with $32$ hardware threads; the software versions are listed in the statement on data and code availability. The largest certified bound is close to $\frac34$ only because a box is accepted as soon as its bound falls below $\frac34$.

\begin{table}[ht]
\centering
\begin{tabular}{@{}lrr@{}}
\toprule
& direct & chart\\
\midrule
initial boxes & $62\,720$ & $73\,728$\\
accepted leaves & $326\,753$ & $18\,574$\\
discarded leaves & $54\,655$ & $55\,188$\\
maximal bisection depth & $10$ & $1$\\
runs of the dependent coordinate & $326\,774$ & $18\,574$\\
largest certified bound $t_{B,X}$ & $0.749999551$ & $0.749865726$\\
evaluations of $P$ (resp.\ $\hat P$) & $17\,422\,672$ & $379\,455$\\
enclosures of $t_y$ (resp.\ $t_Y$) & $645\,551$ & $18\,608$\\
failures & $0$ & $0$\\
wall-clock time & 245\,s & 10\,s\\
\bottomrule
\end{tabular}
\caption{The two computations of Section~\ref{sec:procedure} at the threshold $\frac34$. In the direct computation, $21$ leaves have two runs and all others have one.}\label{tab:runs}
\end{table}

The following checks are not part of the proof.
\begin{enumerate}[label=(\arabic*),leftmargin=2em]
\item \emph{Re-verification of the certificates.} A separate script reads a certificate file and rebuilds every leaf from its initial box and bisection path. For a discarded leaf it repeats the localization and confirms that nothing is kept. For an accepted leaf it confirms that every kept interval lies in a recorded run, and it recomputes the enclosure of $t_y$ on every recorded run with the recorded $y$. This confirmed all $55\,188$ discarded and $18\,574$ accepted leaves of the chart computation (in 7\,s), and all $54\,655$ discarded and $326\,753$ accepted leaves of the direct computation (in 111\,s). The largest recomputed bounds agree with Table~\ref{tab:runs}.
\item \emph{Structure and sampling.} A second script checks that the initial boxes form the grid and that the leaves of every initial box form a complete binary tree, so that they tile it. It then draws $1500$ random points $p$ in each region, finds in floating point all zeros of $P$ (of $\hat P$) above them, and refines these to 40 digits. This gave $273$ convex CCs in the direct region and $288$ in the chart. Each lies in an accepted leaf and in one of its runs, and $\tr S(y)$ there, with the recorded $y$, is below the recorded bound. At each of them $\lmax(G)$ was also computed from an independent formula, which differentiates the areas by the formula $\partial|A_l|/\partial r_e=\frac12r_e\cot\theta$, where $\theta$ is the angle of the triangle opposite the side $e$, instead of Heron's formula, and it never exceeded $\tr S(y)$. In the chart, $t_Y$ agreed with the direct $t_{Y/b}$ to a relative error below $10^{-37}$.
\item \emph{Identities.} The identity $F\prod_es_e=-P$ of Lemma~\ref{lem:dziobekfn}(b) holds at $2000$ random points of $\cC$ to a relative error below $10^{-35}$. At $12$ random convex CCs, the smallest generalized eigenvalue of $(Q,K)$ was computed from finite-difference Hessians of $\Phi$, with the masses of Lemma~\ref{lem:dziobekfn}(c). It agreed with $1-\lmax(G)$ to $12$ digits, as Proposition~\ref{prop:majorant}(c) predicts. The chart formulas of \hyperref[app:chart]{the Appendix} were compared with the direct formulas in computer algebra, with the square roots treated as independent symbols: $h_i$, $\hat P$, $D_e$, $T_e$ and $\beta_e$ agree identically with $g_i/b$ (resp.\ $g_i$), $bP$, $D_e$, $\tau_e/b$ and $\beta_e$. For $\hat P$ and $D_e$, whose expressions are the largest, four of the five values of $\psi$ that occur were also treated as independent symbols; an identity that holds for all values of these symbols holds in particular for the true ones.
\item \emph{The margin.} In floating point, the largest value of $\tr G$ at $200\,000$ random points of each region is $0.5888$ (direct) and $0.5841$ (chart). A local maximization gives $\sup_\cE\tr G\approx0.59270$, approached at the configurations described in Remark~\ref{rem:trace}. The bound $\frac34$ therefore leaves a margin of about $0.157$ for the overestimation in the enclosures. Figure~\ref{fig:lmax} shows $\tr G$ and $\lmax(G)$ at sampled convex CCs.
\end{enumerate}

\begin{figure}[t]
\centering
\includegraphics[width=\textwidth]{fig_lmax.pdf}
\caption{The quantities $\tr G=\min_y\tr S(y)$ (orange) and $\lmax(G)$ (blue) at $21\,985$ sampled normalized convex CCs, plotted against the coordinate $b$ on a logarithmic scale (floating point; an illustration, not part of the proof). The vertical line at $b=\frac18$ separates the direct region from the blow-up chart. The horizontal lines mark the nondegeneracy threshold $1$, the certified bound $\frac34$ for $\tr S$, and the value $\frac13$, the largest limit of $\lmax(G)$ at the corner $b=0$ (Proposition~\ref{prop:corner}).}\label{fig:lmax}
\end{figure}

\subsection{A second implementation}\label{sec:indep}
Proposition~\ref{prop:cap} was also verified by a second program, written from a specification without access to the code of the first.

The specification, which we wrote, restates what the computation needs: the configuration $q(a,b,c,x)$, the closure of the region $\cC$ and the function $F$ of Lemma~\ref{lem:dziobekfn}(b); the formulas for $w_e$, $A_l$, $D_e$, $\tau_e$, $\beta_e$ and $\tr S(y)$; the regions $\Omega_{\mathrm{dir}}$ and $\Omega_{\mathrm{ch}}$; and the substitution of the blow-up chart, with the orders in $b$ of these quantities but not their rescaled forms. It states the two claims of Proposition~\ref{prop:cap}, allows the ranges of $\alpha$ and $\gamma$ in Lemma~\ref{lem:chartbounds} to be taken as given, and mentions that $\tr G$ is at most about $0.59$ on $\cE$. The two programs therefore share the reduction of Sections~\ref{sec:identity} and~\ref{sec:normal}, and in both the conclusion for all of $\cE$ rests on the a priori bounds of Lemmas~\ref{lem:bounds} and~\ref{lem:chartbounds}. They also use the same ball arithmetic library, Arb through \texttt{python-flint}~0.9.0, and they were run on the same machine.

The two programs share no code. The specification forbids reading the first program, and the record of the development, which is included in the repository with the specification, states that only the specification and the second program's own files were used, apart from one text search after all the runs had finished, from which nothing was used. The second program, which takes the threshold as a parameter, differs from the first in the following respects.
\begin{itemize}[leftmargin=2em]
\item It uses its own forward-mode differentiation over Arb balls, at a precision of $96$ bits.
\item It derives the rescaled formulas of the chart itself, and checks them in computer algebra and numerically against the direct formulas.
\item In the direct region it localizes the zeros of the function $F$ of Lemma~\ref{lem:dziobekfn}(b) itself, with $r_e^3=R_e\sqrt{R_e}$, instead of $P$. In the chart it uses $\widetilde F=F/b^2$, which extends analytically to $b=0$ with $\widetilde F(0,\alpha,\gamma,\xi)=\frac94\bigl(3\alpha+3\gamma-3\alpha\gamma+2(1+\gamma)\xi\bigr)$ (compare Lemma~\ref{lem:bzero}).
\item It bounds the trace in sheared coordinates. On a box $B$ with centre $m$, let $x_c$ be a floating-point zero of $F$ above $m$, let $\varphi_k=-\partial_{p_k}F/\partial_xF$ at $(m,x_c)$, and put $x_{\mathrm{lin}}(p)=x_c+\sum_k\varphi_k(p_k-m_k)$. Every zero $(p,x)$ of $F$ with $p\in B$ in the interval under consideration satisfies $\varepsilon=x-x_{\mathrm{lin}}(p)\in E$, for an interval $E$ obtained by interval Newton steps in the variables $(p,\varepsilon)$. The trace is then bounded by a mean-value form in $(p,\varepsilon)$ over $B\times E$. In these variables the derivatives in $p$ are approximately derivatives along the zero set, which are small, so the bound is governed by the width of $E$ rather than by the range of $x$ over $B$.
\item It uses other initial grids ($20\times14\times28$ cubes of side $\frac1{16}$ in the direct region, $8\times24\times24$ boxes of sides $\frac1{64}\times\frac18\times\frac18$ in the chart) and other subdivision rules.
\end{itemize}
Table~\ref{tab:indep} lists its runs at the threshold $\frac34$ and at the smaller threshold $\frac{19}{32}$; all four terminated with every box accepted or discarded. The runs at $\frac{19}{32}$ show that $\tr G<\frac{19}{32}$ on $\cE$, and hence, by Proposition~\ref{prop:majorant}, $Q\ge\frac{13}{32}K$ at every convex CC. The threshold $\frac{19}{32}=0.59375$ is within $0.0011$ of the numerical supremum $0.59270$ of $\tr G$.

\begin{table}[ht]
\centering
\begin{tabular}{@{}llrrrrr@{}}
\toprule
region & threshold & accepted & discarded & max.\ depth & largest bound & time\\
\midrule
direct & $3/4$ & $190\,384$ & $15\,630$ & $13$ & $0.7499990406$ & 42\,s\\
chart & $3/4$ & $20\,189$ & $4\,381$ & $6$ & $0.7499902102$ & 9\,s\\
direct & $19/32$ & $804\,708$ & $42\,166$ & $19$ & $0.5937499913$ & 173\,s\\
chart & $19/32$ & $95\,972$ & $6\,325$ & $10$ & $0.5937499972$ & 41\,s\\
\bottomrule
\end{tabular}
\caption{The second implementation (16 processes). No box was left unproved.}\label{tab:indep}
\end{table}

Two tests support the soundness of the second program. First, a sampling test of its accepted leaves, like check~(2) above, found no failure; at the threshold $\frac{19}{32}$ the smallest gap between a certified bound and the value of $t_Y$ at a sampled CC in the same leaf was $0.0011$ (direct) and $0.0068$ (chart). Second, it was run where the claim fails: on one initial cell of each region that contains a local maximizer of $\tr G$ found in floating point, at thresholds below $\sup_\cE\tr G$, namely $\frac9{16}$ and $\frac{37}{64}$ on the direct cell and $\frac9{16}$ on the chart cell. Within a budget of $4000$ boxes it accepted no box in any of the three runs. At the zeros of $F$ above the centres of the unproved boxes, $\tr G$ took values between $0.5764$ and $0.5918$ in the direct cell and between $0.5832$ and $0.5840$ in the chart cell, so it exceeded the threshold in $1445$ of $1445$ cases (resp.\ $1444$ of $1445$) in the direct cell and in $778$ of $778$ cases in the chart cell.

\section{Proofs of Theorems~B and~A}\label{sec:proofs}

\begin{proof}[Proof of Theorem~B]
Let $q$ be a convex CC for the masses $m$, and let $\pi$, $T$, $(a,b,c,x)\in\cE$, $q'=q(a,b,c,x)$ and $m'$ be as in Lemma~\ref{lem:normal}(b). Write $T(z)=T_0z+t$, where $T_0$ is a real-linear map with $|T_0u|=\nu|u|$ for some $\nu>0$, so that $\ip{T_0u}{T_0u'}=\nu^2\ip{u}{u'}$. Define a linear isomorphism $\Lambda$ of $(\R^2)^4$ by $(\Lambda v)_{\pi(i)}=T_0v_i$. We have $r'_{\pi(i)\pi(j)}=\nu r_{ij}$ and $M'=M$, hence $U(q')=\nu^{-1}U(q)$ and $I(q')=\nu^2I(q)$, and the constant $\lambda'$ of $q'$ equals $\nu^{-3}$ times that of $q$. The corresponding pair potential $\tilde\varphi(r)=\frac1r+\frac{\nu^{-3}\lambda'}{2}r^2$ satisfies $\tilde\varphi(\nu r)=\nu^{-1}\varphi(r)$. Let $\Phi'$ be the function $\Phi$ of $q'$, and let $p\mapsto\tilde p$, $\tilde p_{\pi(i)}=T(p_i)$, be the affine map with linear part $\Lambda$ that sends $q$ to $q'$. Then $\Phi'(\tilde p)=\nu^{-1}\Phi(p)$, and differentiating twice at $q$ gives $Q'(\Lambda v)=\nu^{-1}Q(v)$, where $Q'$ is the form $Q$ of $q'$. Similarly $\kappa'_{\pi(i)\pi(j)}=\nu^{-3}\kappa_{ij}$ and $\dr'_{\pi(i)\pi(j)}(\Lambda v)=\ip{T_0q_{ij}}{T_0v_{ij}}/(\nu r_{ij})=\nu\,\dr_{ij}(v)$, where we used that $\dr_e$ does not depend on the orientation of the edge $e$. Hence $K'(\Lambda v)=\nu^{-1}K(v)$.

By Proposition~\ref{prop:cap} there is $y\in\R^2$ with $\tr S(y)<\frac34$, where $S$ is the matrix of Section~\ref{sec:identity} for the configuration $q'$; if $b\le\frac18$ we apply part (b) and put $y=Y/b$, so that $S(y)=\widehat S(Y)$. By Section~\ref{sec:what}, $S$ is the matrix of the CC $q'$. Proposition~\ref{prop:majorant}(a) gives $Q'\ge(1-\tr S(y))K'\ge\frac14K'$, because $K'\ge0$. Since $\Lambda$ is bijective, $Q\ge\frac14K$. By Lemma~\ref{lem:rigid}, $K(v)>0$ for $v\notin\cT$, so $Q(v)>0$ for $v\notin\cT$. By Lemma~\ref{lem:shape}, $q$ is a nondegenerate local minimum of $f_m$, and its Morse index is $0$.
\end{proof}

\subsection{The covering argument}
Let $\mathcal M=\{m\in(0,\infty)^4:\ m_1+m_2+m_3+m_4=1\}$, an open convex subset of an affine hyperplane, and let
\[
\cS^+=\{[q]\in\cS:\ A_1(q)>0,\ A_2(q)<0,\ A_3(q)>0,\ A_4(q)<0\}.
\]
By Lemma~\ref{lem:areas}(b) the signs of the $A_l$ depend only on the class $[q]$, so $\cS^+$ is a well-defined open subset of $\cS$. By Lemma~\ref{lem:areas}(c) it is disjoint from $\Delta$. If all $A_l$ are nonzero, then no three of the $q_l$ are collinear. So, by Lemma~\ref{lem:areas}(d), $\cS^+$ is the set of classes of counterclockwise strictly convex quadrilaterals with vertices $q_1,q_2,q_3,q_4$ in this order. Complex conjugation induces a real-analytic involution $\iota[q]=[\bar q]$ of $\cS$, which is well defined because $\overline{\mu q+t\mathbb 1}=\bar\mu\bar q+\bar t\mathbb 1$. It preserves $\Delta$ and satisfies $f_m\circ\iota=f_m$. By Lemma~\ref{lem:areas}(b) it maps $\cS^+$ onto the set where all four signs are reversed, which is disjoint from $\cS^+$.

The function $f(s,m)=f_m(s)$ is real-analytic on $(\cS\setminus\Delta)\times(0,\infty)^4$. Let
\[
\cZ=\{(s,m)\in\cS^+\times\mathcal M:\ s\text{ is a critical point of }f_m\},
\]
and let $\mathrm{pr}:\cZ\to\mathcal M$ be the projection. By Section~\ref{sec:shape}, $\mathrm{pr}^{-1}(m)$ is in bijection with the set of classes of counterclockwise convex CCs with cyclic order $(1234)$ for the masses $m$.

\begin{lemma}\label{lem:local}
$\cZ$ is a real-analytic submanifold of $\cS^+\times\mathcal M$ of dimension $3$, and $\mathrm{pr}$ is a local real-analytic diffeomorphism.
\end{lemma}

\begin{proof}
Let $(s_0,m_0)\in\cZ$, and choose a real-analytic chart $\chi$ of $\cS^+$ near $s_0$. Near $(s_0,m_0)$, the set $\cZ$ is the zero set of the map $(u,m)\mapsto\nabla_uf(\chi^{-1}(u),m)\in\R^4$. Its derivative with respect to $u$ at $(\chi(s_0),m_0)$ is the matrix of $D^2f_{m_0}(s_0)$ in the chart. This matrix is invertible by Theorem~B, since $s_0$ is the class of a convex CC. By the real-analytic implicit function theorem there are neighbourhoods $\mathcal U$ of $s_0$ and $\mathcal N$ of $m_0$ and a real-analytic map $g:\mathcal N\to\mathcal U$ such that $\cZ\cap(\mathcal U\times\mathcal N)$ is the graph of $g$. The claims follow.
\end{proof}

\begin{lemma}\label{lem:shub}
Let $m^n\in(0,\infty)^4$ converge to $m^\infty\in(0,\infty)^4$. For each $n$ let $q^n$ be a CC for the masses $m^n$ with centre of mass $0$ and $I(q^n)=1$, both computed with the masses $m^n$. Then a subsequence of $(q^n)$ converges to a CC $q^\infty$ for the masses $m^\infty$. In particular $q^\infty$ is collision-free.
\end{lemma}

For fixed masses this is Shub's lemma \cite{Shu71}, which says that the CCs stay away from the collisions. We follow the proof in \cite[Proposition~15]{Moe15}, and include it because here the masses vary.

\begin{proof}
Write $U_n$ for the potential with the masses $m^n$, and $\lambda_n=U_n(q^n)$ for the multiplier of $q^n$. Since $m^n_i|q^n_i|^2\le I(q^n)=1$ and $m^n_i\to m^\infty_i>0$, the sequence is bounded, and after passing to a subsequence $q^n\to q^\infty$. By continuity, $q^\infty$ has centre of mass $0$ and $I(q^\infty)=1$ for the masses $m^\infty$. In particular the $q^\infty_i$ are not all equal. Suppose that $q^\infty$ has a collision. Group the indices into clusters $\Gamma$, consisting of indices with a common limit position $p_\Gamma$. Some $r^n_{ij}$ tends to $0$, so $\lambda_n\to\infty$. Sum \eqref{eq:cc} over $i\in\Gamma$. The mutual forces between the bodies of $\Gamma$ cancel in pairs, and the forces exerted by the other bodies stay bounded, because their distances to the bodies of $\Gamma$ have positive limits. Hence $\lambda_n\sum_{i\in\Gamma}m^n_iq^n_i$ is bounded, and $\sum_{i\in\Gamma}m^n_iq^n_i\to0$. The limit of this sum is $(\sum_{i\in\Gamma}m^\infty_i)\,p_\Gamma$, so $p_\Gamma=0$ for every cluster $\Gamma$. Different clusters have different limit positions, so there is only one cluster, and $q^\infty_i=0$ for all $i$. This is a contradiction, so $q^\infty$ is collision-free. Then $\lambda_n\to U_\infty(q^\infty)$, where $U_\infty$ is the potential with the masses $m^\infty$, and letting $n\to\infty$ in \eqref{eq:cc} shows that $q^\infty$ is a CC for $m^\infty$.
\end{proof}

The next lemma is a second application of Theorem~B.

\begin{lemma}\label{lem:collinear}
Let $q^n$ be convex CCs for masses $m^n\in(0,\infty)^4$. Suppose that $m^n\to m\in(0,\infty)^4$ and that $q^n$ converges to a CC $q$ for the masses $m$. Then $q$ is not collinear.
\end{lemma}

\begin{proof}
Suppose that $q$ lies on a line with unit direction $u$. Let $k$ be the body with the largest coordinate $\ip{q_j}{u}$, write $r_j=r_{kj}$, and let all sums run over $j\ne k$. Then $q_k-q_j=r_ju$ for $j\ne k$, and the three distances $r_j$ are distinct, because $q$ is collision-free. Let $v\in(\R^2)^4$ move $q_k$ by $Ju$ and leave the other bodies fixed. Then $\dr_e(v)=0$ for every edge $e$, so $K(v)=0$, and Lemma~\ref{lem:hessian}(a) gives
\[
Q(v)=-\sum\omega_{kj}=-m_k\sum m_j\,(s_{kj}-\lambda').
\]
The component of \eqref{eq:equil} for $i=k$ along $u$ is $\sum m_j(s_{kj}-\lambda')r_j=0$. So $\lambda'=\sum m_jr_j^{-2}/\sum m_jr_j$, and
\begin{align*}
\Bigl(\sum m_jr_j\Bigr)\sum m_j(s_{kj}-\lambda')&=\Bigl(\sum m_jr_j^{-3}\Bigr)\Bigl(\sum m_jr_j\Bigr)-\Bigl(\sum m_jr_j^{-2}\Bigr)\Bigl(\sum m_j\Bigr)\\
&=\frac12\sum_{i,j\ne k}m_im_j\,(r_j-r_i)(r_i^{-3}-r_j^{-3}).
\end{align*}
The terms of the last sum are nonnegative, and they are positive when $r_i\ne r_j$. So $Q(v)<0$. On the other hand, let $Q_n$ and $K_n$ be the forms $Q$ and $K$ of the CC $q^n$ for the masses $m^n$. By Theorem~B, $Q_n(v)\ge\frac14K_n(v)\ge0$. At collision-free configurations the multiplier $\lambda=U/I$ depends continuously on the configuration and the masses, and hence so do $\kappa_e$, $\omega_e$ and $\dr_e(v)$ in Lemma~\ref{lem:hessian}(a). So $Q_n(v)\to Q(v)$, and $Q(v)\ge0$, a contradiction.
\end{proof}

\begin{lemma}\label{lem:proper}
The projection $\mathrm{pr}:\cZ\to\mathcal M$ is proper.
\end{lemma}

\begin{proof}
Let $C\subset\mathcal M$ be compact, and let $(s_n,m_n)$ be a sequence in $\mathrm{pr}^{-1}(C)$. After passing to a subsequence, $m_n\to m^\infty\in C$. Represent $s_n$ by a CC $q^n$ for $m_n$ with centre of mass $0$ and $I(q^n)=1$. By Lemma~\ref{lem:shub}, after passing to a further subsequence, $q^n$ converges to a CC $q^\infty$ for $m^\infty$, and $s_n\to s_\infty=[q^\infty]\in\cS\setminus\Delta$. Since $s_n\in\cS^+$, the $q^n$ are convex CCs, so $q^\infty$ is not collinear by Lemma~\ref{lem:collinear}. By Lemma~\ref{lem:nocollinear} no three of the $q^\infty_l$ are collinear, and by Lemma~\ref{lem:areas}(d) all $A_l(q^\infty)$ are nonzero. As limits of the $A_l(q^n)$ they have the signs $(+,-,+,-)$. Hence $s_\infty\in\cS^+$, and $(s_\infty,m^\infty)\in\mathrm{pr}^{-1}(C)$. Thus every sequence in $\mathrm{pr}^{-1}(C)$ has a subsequence that converges in $\mathrm{pr}^{-1}(C)$. Since $\cZ$ is metrizable, $\mathrm{pr}^{-1}(C)$ is compact.
\end{proof}

\begin{lemma}\label{lem:count}
Let $p:X\to Y$ be a proper local homeomorphism between metrizable spaces, with $Y$ connected. Then all fibres of $p$ are finite and have the same number of points.
\end{lemma}

\begin{proof}
A fibre $p^{-1}(y)$ is compact because $p$ is proper, and discrete because $p$ is a local homeomorphism. So it is finite, say $p^{-1}(y)=\{x_1,\dots,x_k\}$. Choose pairwise disjoint open sets $U_i\ni x_i$ such that $p$ maps $U_i$ homeomorphically onto an open set $V_i\ni y$, and put $F=X\setminus\bigcup_iU_i$. The set $p(F)$ is closed. Indeed, if $p(x_n)\to z$ with $x_n\in F$, then the $x_n$ lie in the compact set $p^{-1}(\{z\}\cup\{p(x_n):n\ge1\})$, so a subsequence converges to a point $x\in F$ with $p(x)=z$. Also $y\notin p(F)$. So $W=\bigcap_iV_i\setminus p(F)$ is an open neighbourhood of $y$ (if $k=0$, then $W=Y\setminus p(F)$). For $z\in W$ the fibre $p^{-1}(z)$ lies in $\bigcup_iU_i$ and meets each $U_i$ in exactly one point, so it has $k$ points. Hence the number of points in the fibres is locally constant, and therefore constant.
\end{proof}

\begin{proof}[Proof of Theorem~A]
By Lemmas~\ref{lem:local}, \ref{lem:proper} and~\ref{lem:count}, the number $N(m)$ of points of $\mathrm{pr}^{-1}(m)$ is finite and independent of $m\in\mathcal M$. For four equal masses, the only convex CC up to similarity is the square. Indeed, let $q$ be such a CC with cyclic order $(1234)$. By \cite[Theorem~1]{AFS08}, applied to both diagonals, $q$ is symmetric with respect to the lines $q_1q_3$ and $q_2q_4$, so that $A_1=A_3$ and $A_2=A_4$. By Lemma~\ref{lem:areas}(a), the four numbers $|A_l|$ are then equal. By \eqref{eq:dziobek}, $s_{ij}=\lambda'+\sigma A_iA_j/(m_im_j)$ takes one value on the four sides and another on the two diagonals, so $q$ is a rhombus with equal diagonals, that is, a square. A counterclockwise square with vertices $q_1,q_2,q_3,q_4$ in this order and centre $o$ satisfies $q_k-o=J^{k-1}(q_1-o)$. So it equals $(q_1-o)(1,J,-1,-J)+o\mathbb 1$, and its class is the class of $(1,J,-1,-J)$, which lies in $\cS^+$. Hence $N(\frac14,\frac14,\frac14,\frac14)=1$, and so $N\equiv1$. By Lemma~\ref{lem:local}, $\mathrm{pr}$ is then a bijective local real-analytic diffeomorphism, hence a real-analytic diffeomorphism. Its inverse has the form $m\mapsto(s(m),m)$, with $s:\mathcal M\to\cS^+$ real-analytic.

Now let $m\in(0,\infty)^4$, put $\hat m=m/\sum_im_i$, and let $q$ be a convex CC for $m$ with cyclic order $(1234)$. It is also a CC for $\hat m$. If $q$ is counterclockwise, then $[q]$ corresponds to a point of $\mathrm{pr}^{-1}(\hat m)$, so $[q]=s(\hat m)$. If $q$ is clockwise, then $\bar q$ is a counterclockwise convex CC with the same cyclic order, and $[q]=\iota(s(\hat m))$. The classes $s(\hat m)$ and $\iota(s(\hat m))$ are distinct, because the signs of the $A_l$ differ, and they are mirror images of each other. So there are exactly two convex CCs with cyclic order $(1234)$ up to orientation-preserving similarity, and exactly one up to similarity. Both are nondegenerate local minima of $f_m$ by Theorem~B, and both depend real-analytically on $m$. For the cyclic orders $(1243)$ and $(1324)$, exchange the labels $3$ and $4$, respectively $2$ and $3$, together with the corresponding masses.
\end{proof}

\begin{remark}\label{rem:existence}
The existence part of this argument, $N\ge1$, uses only the elementary fact that the square is a CC for four equal masses. Theorem~B and the covering argument therefore also give a proof of the theorem of MacMillan and Bartky \cite{MB32} that convex CCs with every cyclic order exist for all masses; compare \cite{Xia04}. The theorem of Albouy, Fu and Sun is needed only for $N\le1$.
\end{remark}

\subsection{A formal proof}\label{sec:lean}
Theorems~A and~B have been formalized in the proof assistant Lean~4 with the Mathlib library; see the statement on data and code availability. The formalization constructs the shape space as in Section~\ref{sec:shape}, as the quotient of the configurations that are not totally collapsed by the orientation-preserving similarities, with the affine charts $q_i=0$, $q_j=1$. It proves that $\cS$ is a compact Hausdorff real-analytic manifold of dimension~$4$, that $f_m$ is real-analytic on $\cS\setminus\Delta$, and that the critical points of $f_m$ are the classes of the CCs. The identification with $\C P^2$ is not formalized, and it is not used. The Hessian of $f_m$ at a critical point is read in a chart, and with these definitions Theorems~A and~B and the sentence that follows Theorem~A are formalized as stated. For the analytic dependence on the masses the formal statement is Corollary~C(i): for each cyclic order and orientation there is a map from $(0,\infty)^4$ to $\cS$, real-analytic for this manifold structure, that sends $m$ to the class of the convex CC with that cyclic order and orientation. The formal proof obtains this map from a real-analytic representative in $(\R^2)^4$, which it constructs in the slice $q_1=0$, $q_2=1$ from Theorem~B and the implicit function theorem for real-analytic maps, which is part of Mathlib. The formal proof of uniqueness needs only that $\mathrm{pr}$ is a local homeomorphism, which it derives from Theorem~B and the implicit function theorem.

The formalization also contains most of the other results of Sections~\ref{sec:prelim}, \ref{sec:identity}, \ref{sec:normal} and~\ref{sec:cons}: Lemmas~\ref{lem:hessian}, \ref{lem:shape} and~\ref{lem:areas}; Lemma~\ref{lem:rigid}, except the statements on the rank and the image of $\dr$; Lemmas~\ref{lem:nocollinear} and~\ref{lem:dziobek}; Propositions~\ref{prop:convexsigns} and~\ref{prop:identity}; Corollary~\ref{cor:palmore}; Lemmas~\ref{lem:dziobekfn} and~\ref{lem:normal}; Corollary~C(ii) and the first two sentences of~(iii); and Corollary~D. In Lean the form $Q$ is defined by the formula of Lemma~\ref{lem:hessian}(a), and part~(a) is the statement that this form is $D^2\Phi(q)$, which holds at every collision-free $q$. In these statements, the hypothesis that no three bodies are collinear takes the form that no $A_l$ vanishes, and a CC is called noncollinear if some $A_l$ is nonzero, which is equivalent by Lemma~\ref{lem:areas}(c). The formal statement of Lemma~\ref{lem:areas}(d) expresses that $q_1,q_2,q_3,q_4$ are the vertices of a strictly convex quadrilateral in this cyclic order by the condition that the open segments $q_1q_3$ and $q_2q_4$ meet and are not parallel. The other formal statements define convexity and the cyclic order by the signs of the $A_l$, and Lemma~\ref{lem:areas}(d) shows that this agrees with the geometric definition. Not formalized are Corollary~C(iv) and the last sentence of~(iii), which use results of \cite{Moe15} on collinear CCs and on the topology of $\cS\setminus\Delta$, Proposition~\ref{prop:corner}, and Remarks~\ref{rem:identity}(ii) and~\ref{rem:involution}.

The development contains no unproved statements, and it uses no axioms besides the three standard axioms of Lean (propositional extensionality, the axiom of choice and the soundness of quotients); Lean's command \texttt{\#print axioms} lists exactly these three for each of the formal statements. In particular, the computation is checked by the kernel of Lean, the small program that checks every proof, and not by compiled code, whose use Lean would record as an additional axiom. The computation is a branch and bound written in Lean, a third implementation of Proposition~\ref{prop:cap}, which uses interval arithmetic with directed rounding on the fixed-point numbers $n2^{-96}$ with integer $n$, slope enclosures (a variant of the mean-value enclosures of Section~\ref{sec:balls}), and localization by interval Newton steps and bisection, starting from the initial grids of Table~\ref{tab:runs}. The search was run beforehand by an unverified program, which records its decisions (where to bisect, how to localize, and which $y$ or $Y$ to use) in a hint for each initial box. The formal proof replays the hints and checks every step, so a wrong hint can only make the check fail. The replay is split into $3418$ Boolean statements, each about a block of consecutive initial boxes, and each is proved by the tactic \texttt{decide +kernel}, which evaluates it in the kernel. All the facts about the computation that the argument uses are proved in Lean:
\begin{itemize}[leftmargin=2em]
\item the soundness of the arithmetic, of the enclosures and of the replay;
\item the fact that the initial boxes cover the regions of Lemmas~\ref{lem:bounds} and~\ref{lem:chartbounds}, which are also proved in Lean;
\item the fact that the certified functions are the traces $\tr S(y)$ and $\tr\widehat S(Y)$ of Section~\ref{sec:what}.
\end{itemize}
In these evaluations the kernel uses its built-in arithmetic of natural numbers, which is implemented with the GMP library and is part of the standard kernel. The evaluations take about $7.6$ hours of processor time, or about $19$ minutes on a machine with $32$ hardware threads, and the rest of the development is checked in about two minutes. As an independent check, the formal proof has also been checked by nanoda, a second type checker for Lean, written in Rust and with its own arithmetic of natural numbers. It checked each of the $211$ files of Boolean statements with only the three standard axioms, and the rest of the proof with the $3418$ statements as axioms; a script checks that the two parts fit together, by comparing hashes of the statements and of the definitions that they share.

The formal proof follows Sections~\ref{sec:prelim}--\ref{sec:proofs}, with three differences.
\begin{enumerate}[label=\textup{(\roman*)},leftmargin=2.2em]
\item The covering argument works in the slice $q_1=0$, $q_2=1$, that is, in one chart of $\cS$, where the CCs are the zeros of the equations of the bodies $3$ and $4$.
\item Lemma~\ref{lem:count} is derived from the theorem in Mathlib that a proper local homeomorphism is a covering map.
\item It does not assume \cite[Theorem~1]{AFS08}. For four equal masses it proves $A_1=A_3$ and $A_2=A_4$ directly, following the proof in \cite{AFS08}.
\end{enumerate}
The analytic core of that proof is \cite[Lemma~2]{AFS08}, an inequality stated for every negative exponent $\alpha$. For the Newtonian exponent $\alpha=-\frac23$ it reduces to the polynomial inequality
\[
(U+V)(U^3+V^3-2U^3V^3)\le U^2+UV+V^2,\qquad 0\le U,V\le1 .
\]
The difference of the two sides equals $U^2(1-U^2)+V^2(1-V^2)+UV(1-U^2)(1-V^2)+U^3V^3(2U+2V-1)$. Every term is nonnegative if $2U+2V\ge1$. Otherwise $U,V<\frac12$, and the last term is at least $-U^3V^3\ge-\frac9{16}UV\ge-UV(1-U^2)(1-V^2)$.

\section{Consequences and open questions}\label{sec:cons}

\subsection{Proof of Corollary~C}
(i) By the proof of Theorem~A, the counterclockwise and the clockwise convex CC with cyclic order $(1234)$ are the classes $s(\hat m)$ and $\iota(s(\hat m))$, where $\hat m=m/\sum_im_i$. Both depend real-analytically on $m$. For the other cyclic orders, relabel the bodies.

(ii) For $z\in\cE$ let $\mathfrak m(z)\in\mathcal M$ be the masses of Lemma~\ref{lem:dziobekfn}(c), normalized so that their sum is $1$. Suppose that $\mathfrak m(z)=\mathfrak m(z')=m$. By Lemma~\ref{lem:normal}(a), $q(z)$ and $q(z')$ are counterclockwise convex CCs with cyclic order $(1234)$ for the masses $m$. So $([q(z)],m)$ and $([q(z')],m)$ lie in $\mathrm{pr}^{-1}(m)$, which consists of the single point $(s(m),m)$ by the proof of Theorem~A. Hence $[q(z)]=[q(z')]$, and $z=z'$ by Lemma~\ref{lem:normal}(c). Any other normalization of the masses, for instance $m_1=1$, gives an equivalent statement.

As a consistency check, let $z=(a,b,c,x)\in\cE$, and suppose that the masses of $q(z)$ satisfy $m_1=m_2$ and $m_3=m_4$. The involution of Remark~\ref{rem:involution} maps $z$ to a point of $\cE$ with the same normalized masses, so by (ii) it fixes $z$. Hence $a=1$ and $b=c$, so that $q_3=-b\,q_1$ and $q_4=-b\,q_2$. Since $|q_1|=|q_2|=1$, the reflection in the perpendicular bisector of $q_1q_2$ is linear. It exchanges $q_1$ and $q_2$, and hence also $q_3$ and $q_4$. So $q(z)$ is an isosceles trapezoid with $q_1q_2\parallel q_3q_4$, in accordance with Corollary~D(b).

(iii) A similarity preserves the cyclic order of a convex configuration. By Theorem~A there are therefore exactly three convex CCs up to similarity, one for each cyclic order. Each of them gives two classes up to orientation-preserving similarity, the configuration and its mirror image, which are distinct by Lemma~\ref{lem:areas}(b). This gives six. All of them are nondegenerate local minima by Theorem~B.

Now suppose that all concave CCs for the masses $m$ are nondegenerate. Collinear CCs are nondegenerate, of Morse index $2$ \cite[Proposition~19]{Moe15}, and convex CCs are nondegenerate by Theorem~B. So $f_m$ is a Morse function on $\cS\setminus\Delta$. It is positive and tends to $+\infty$ at $\Delta$, so its sublevel sets are compact. Its critical set is compact by Lemma~\ref{lem:shub}, applied with constant masses, and it consists of isolated points, so it is finite. The Morse inequalities \cite[Section~11]{Moe15}, \cite{Pac87} compare the numbers $\gamma_k$ of critical points of index $k$ with the Betti numbers of $\cS\setminus\Delta$, whose Poincaré polynomial is $1+5t+6t^2$ \cite[Proposition~24]{Moe15}. By Corollary~\ref{cor:palmore} all indices are at most $2$, so
\[
\gamma_0+\gamma_1t+\gamma_2t^2=1+5t+6t^2+(1+t)(r_0+r_1t)
\]
with $r_0,r_1\ge0$. Hence $\gamma_0=1+r_0$, $\gamma_1=5+r_0+r_1$, $\gamma_2=6+r_1$, and the total number of CCs is $12+2(r_0+r_1)$. The six convex CCs give $\gamma_0\ge6$, and the twelve collinear CCs \cite[Propositions~18 and~19]{Moe15} give $\gamma_2\ge12$. So $r_0\ge5$ and $r_1\ge6$, and there are at least $34$ CCs up to orientation-preserving similarity. This is the argument of \cite[Section~13]{Moe15}, where all CCs are assumed to be nondegenerate. By Theorem~B the assumption is needed only for the concave CCs.

(iv) By Lemmas~\ref{lem:nocollinear} and~\ref{lem:areas}(d), a planar CC is collinear, convex or concave. Collinear CCs are nondegenerate \cite[Proposition~19]{Moe15}, \cite{Pac87}, and convex CCs are nondegenerate by Theorem~B. \qed

\subsection{Proof of Corollary~D}
The hypotheses and the conclusions are invariant under reflections, so we may assume that $q$ is counterclockwise. By the proof of Theorem~A, two counterclockwise convex CCs with cyclic order $(1234)$ for the same masses differ by an orientation-preserving similarity $T(z)=\mu z+t$. If such a $T$ fixes two distinct points, then $T$ is the identity.

(a) Let $\mathfrak r$ be the reflection in the line $q_2q_4$. Then $\mathfrak rq$ is a clockwise convex CC for the masses $m$. Exchanging the labels $1$ and $3$, we see that $q'=(\mathfrak rq_3,q_2,\mathfrak rq_1,q_4)$ is a CC for the masses $(m_3,m_2,m_1,m_4)=m$. It traverses the vertices of $\mathfrak rq$ in the order $3,2,1,4$, the reverse of their order in $\mathfrak rq$. So $q'$ is a counterclockwise convex CC with cyclic order $(1234)$, and $q'_i=T(q_i)$ for an orientation-preserving similarity $T$. Since $T$ fixes $q_2$ and $q_4$, it is the identity, and $\mathfrak rq_3=q_1$. So $q$ is symmetric with respect to the diagonal $q_2q_4$.

(b) Let $\mathfrak r$ be the reflection in the perpendicular bisector of $q_1q_2$, so that $\mathfrak rq_1=q_2$ and $\mathfrak rq_2=q_1$. Exchanging the labels $1\leftrightarrow2$ and $3\leftrightarrow4$ in $\mathfrak rq$ gives the CC $q'=(\mathfrak rq_2,\mathfrak rq_1,\mathfrak rq_4,\mathfrak rq_3)=(q_1,q_2,\mathfrak rq_4,\mathfrak rq_3)$ for the masses $(m_2,m_1,m_4,m_3)=m$. It traverses the vertices of $\mathfrak rq$ in the order $2,1,4,3$, which is again the reverse order. As in (a), $q'_i=T(q_i)$, where now $T$ fixes $q_1$ and $q_2$. So $T$ is the identity and $\mathfrak rq_4=q_3$. Thus $\mathfrak r$ exchanges $q_3$ and $q_4$. Hence $q_3q_4$ is perpendicular to the axis of $\mathfrak r$, like $q_1q_2$, and $r_{14}=r_{23}$. So $q$ is an isosceles trapezoid with $q_1q_2\parallel q_3q_4$.

(c) By (a), $q$ is symmetric with respect to the line $q_2q_4$. The configuration $(q_2,q_3,q_4,q_1)$, with the masses $(m_2,m_3,m_4,m_1)$, is a convex CC with cyclic order $(1234)$ whose first and third masses are equal. By (a) it is symmetric with respect to the line $q_3q_1$. So each diagonal lies on the perpendicular bisector of the other. The diagonals therefore bisect each other and are perpendicular, and $q$ is a rhombus. \qed

\begin{remark}\label{rem:dias}
Dias \cite[Lemma~7.7]{Dia26} reads the equations of a CC as an equilibrium stress of the configuration, which is a positive multiple of our self-stress $\omega$. For strictly convex planar CCs that satisfy a sign condition of MacMillan--Bartky type \cite[Definition~7.8]{Dia26}, Dias shows that the associated stress matrix is positive semidefinite of rank $n-3$, so that these CCs are not vertically degenerate in the sense of \cite{Dia26} \cite[Corollary~7.12]{Dia26}. For $n=4$ the sign condition is Proposition~\ref{prop:convexsigns}(a); compare \cite[Corollary~7.10]{Dia26}. In this case Remark~\ref{rem:identity}(ii) gives the stress matrix explicitly: its entries are $\Omega_{ij}=-\omega_{ij}=|\sigma|A_iA_j$ for $i\ne j$ and $\Omega_{ii}=\sum_{j\ne i}\omega_{ij}=|\sigma|A_i^2$, so $\Omega=|\sigma|AA^{\mathsf T}$, for convex and concave CCs alike, and the stress energy is $|\sigma|\,|L|^2$. The two statements are complementary: vertical degeneracy concerns higher dimensions, whereas Theorem~B concerns the planar second variation. The rank-one structure alone does not control the sign of $Q=K-|\sigma||L|^2$; this requires the comparison with $K$ in Proposition~\ref{prop:majorant}.
\end{remark}

\subsection{The corner and the optimal constant}
Let $\theta^*$ be the largest constant $\theta$ such that $Q\ge\theta K$ at every convex CC. By Proposition~\ref{prop:majorant}(c), $\theta^*=1-\sup\lmax(G)$, where the supremum is taken over all convex CCs, and by Section~\ref{sec:indep}, $\theta^*\ge\frac{13}{32}$.

\begin{proposition}\label{prop:corner}
Let $\frac12<\gamma_*<2$ and $-\frac{\gamma_*}2<\alpha_*<\frac12$, put $\rho_*=(\gamma_*^2-\gamma_*+1)^{1/2}$, and
\begin{gather*}
h_1^*=\frac{(1-2\alpha_*)(2-\gamma_*)}{1+\gamma_*},\qquad h_2^*=\frac{(2\alpha_*+\gamma_*)(2\gamma_*-1)}{1+\gamma_*},\\
h_3^*=\frac{(2\alpha_*+\gamma_*)(2-\gamma_*)}{1+\gamma_*},\qquad h_4^*=\frac{(1-2\alpha_*)(2\gamma_*-1)}{1+\gamma_*}.
\end{gather*}
\begin{enumerate}[label=\textup{(\alph*)},leftmargin=2em]
\item Let $\xi(b,\alpha,\gamma)$ be the function of Lemma~\ref{lem:bzero} near $(0,\alpha_*,\gamma_*)$. For all sufficiently small $b>0$ the point $z_b=\bigl(1+b\alpha_*,\,b,\,b\gamma_*,\,\frac12+b\,\xi(b,\alpha_*,\gamma_*)\bigr)$ lies in $\cE$.
\item Normalize the masses of $q(z_b)$ by $\sigma=-1$. As $b\to0$,
\begin{gather*}
m_1m_3\to\frac1{8h_1^*},\qquad m_1m_4\to\frac1{8h_3^*},\qquad m_2m_3\to\frac{\gamma_*}{8h_4^*},\qquad m_2m_4\to\frac{\gamma_*}{8h_2^*},\\
b^3m_1m_2\to\frac{\gamma_*}{12h_1^*h_2^*\rho_*^3},\qquad \frac{m_3m_4}{b^3}\to\frac{3\rho_*^3}{16},
\end{gather*}
and hence
\[
\frac{m_1}{m_2}\to\frac{2\gamma_*-1}{\gamma_*(2-\gamma_*)},\qquad \frac{m_3}{m_4}\to\frac{\gamma_*+2\alpha_*}{1-2\alpha_*},\qquad \frac{m_3}{b^3m_1}\to\frac32\rho_*^3h_3^*,\qquad \frac{m_4}{b^3m_2}\to\frac{3\rho_*^3h_4^*}{2\gamma_*}.
\]
The map from $(\alpha_*,\gamma_*)$ to the limits of $m_1/m_2$ and $m_3/m_4$ is a bijection onto $(0,\infty)^2$.
\item The matrix $G$ of $q(z_b)$ converges as $b\to0$ to a matrix $G_0$ that depends only on $\gamma_*$ and has the eigenvalues $\frac14$ and
\[
\mu(\gamma_*)=\frac{(2\gamma_*-1)(2-\gamma_*)}{3\gamma_*}=\frac13-\frac{2(\gamma_*-1)^2}{3\gamma_*}.
\]
Hence $\lmax(G)\to\max\bigl(\frac14,\mu(\gamma_*)\bigr)\le\frac13$, with equality if and only if $\gamma_*=1$.
\item $\theta^*\le\frac23$. More precisely, if $\gamma_*=1$, the smallest generalized eigenvalue of $(Q,K)$ at $q(z_b)$ tends to $\frac23$. For $\alpha_*=0$ and $\gamma_*=1$ the configurations $q(z_b)=q(1,b,b,x_b)$, $x_b=\frac12+b\,\xi(b,0,1)$, are isosceles trapezoids, with $m_1=m_2$, $m_3=m_4$ and $m_3/m_1\sim\frac34b^3$.
\end{enumerate}
\end{proposition}

So every pair of limiting ratios $m_1/m_2$, $m_3/m_4$ occurs at the corner, and there the two masses $m_3,m_4$ are of order $b^3$ relative to $m_1,m_2$.

\begin{proof}
We drop the asterisks. At $b=0$ and $\xi=\xi(0,\alpha,\gamma)=\frac{3(\alpha\gamma-\alpha-\gamma)}{2(1+\gamma)}$, the formulas of Section~\ref{sec:chart} give $h_i=h_i^*$ for $i\le4$ and $h_5=h_6=1$. These values are positive under our hypotheses, and they satisfy
\[
h_1+h_3=2-\gamma,\qquad h_2+h_4=2\gamma-1,\qquad h_1h_2=h_3h_4 .
\]
All quantities below are given by the formulas of Section~\ref{sec:chart} and \hyperref[app:chart]{the Appendix}. These are real-analytic near $(0,\alpha,\gamma,\xi(0,\alpha,\gamma))$, so their limits along $z_b$ as $b\to0$ are their values at $b=0$.

(a) By continuity, $h_1,\dots,h_6>0$ at $(b,\alpha,\gamma,\xi(b,\alpha,\gamma))$ for all small $b>0$, and $\hat P=0$ there by Lemma~\ref{lem:bzero}. Hence $g_i=b\,h_i>0$ for $i\le4$, $g_5,g_6>0$ and $P=\hat P/b=0$. Moreover $a=1+b\alpha>0$, $c=b\gamma>0$ and $|x|<1$ for small $b$. So $z_b\in\cE$.

(b) At $b=0$ we have $x=\frac12$, $s=\frac{\sqrt3}2$, $R_e=1$ for $e\ne34$, $\psi=\frac32$ and $a+c=1$. Hence
\[
\hat\eta_{13}=\tfrac32h_1,\qquad\hat\eta_{24}=\tfrac32h_2,\qquad\hat\eta_{14}=\tfrac32h_3,\qquad\hat\eta_{23}=\tfrac32h_4,\qquad\hat\eta_{34}=\hat\delta=\rho^{-3},
\]
and the formulas of \hyperref[app:chart]{the Appendix} give
\begin{gather*}
\hw_{12}=\tfrac94h_1h_2\rho^3,\quad\hw_{13}=-\tfrac32h_1,\quad\hw_{24}=-\tfrac32h_2,\quad\hw_{14}=\tfrac32h_3,\quad\hw_{23}=\tfrac32h_4,\quad\hw_{34}=\rho^{-3},\\
\hA_1=A_3=\tfrac{\sqrt3}4,\qquad\hA_2=-\tfrac{\sqrt3}4\gamma,\qquad A_4=-\tfrac{\sqrt3}4 .
\end{gather*}
By Lemma~\ref{lem:dziobekfn}(c) and the scalings of Section~\ref{sec:chart},
\begin{gather*}
m_1m_2=-b^{-3}\frac{\hA_1\hA_2}{\hw_{12}},\qquad m_3m_4=-b^3\frac{A_3A_4}{\hw_{34}},\qquad m_1m_3=-\frac{\hA_1A_3}{\hw_{13}},\\
m_1m_4=-\frac{\hA_1A_4}{\hw_{14}},\qquad m_2m_3=-\frac{\hA_2A_3}{\hw_{23}},\qquad m_2m_4=-\frac{\hA_2A_4}{\hw_{24}} .
\end{gather*}
Inserting the values at $b=0$ gives the six limits. The four ratios follow from
\[
\frac{m_1}{m_2}=\frac{m_1m_3}{m_2m_3},\qquad\frac{m_3}{m_4}=\frac{m_1m_3}{m_1m_4},\qquad\frac{m_3}{m_1}=\frac{m_2m_3}{m_1m_2},\qquad\frac{m_4}{m_2}=\frac{m_1m_4}{m_1m_2},
\]
together with $h_1h_2=h_3h_4$ and the explicit form of the $h_i^*$. Finally, $\gamma\mapsto(2\gamma-1)/(\gamma(2-\gamma))$ maps $(\frac12,2)$ onto $(0,\infty)$ and has the derivative $2(\gamma^2-\gamma+1)/(2\gamma-\gamma^2)^2>0$. For fixed $\gamma$, $\alpha\mapsto(\gamma+2\alpha)/(1-2\alpha)$ maps $(-\frac\gamma2,\frac12)$ onto $(0,\infty)$ and has the derivative $2(1+\gamma)/(1-2\alpha)^2>0$.

(c) We have $c_0=b^2\hat c_0$ and $b_0=b\,\hat b_0$, where $\hat c_0=\sum_eD_eT_e^2$ and $\hat b_0=\sum_eD_eT_e\beta_e$. Hence $G=\sum_eD_e\beta_e\beta_e^{\mathsf T}-\hat c_0^{-1}\hat b_0\hat b_0^{\mathsf T}$. At $b=0$, \hyperref[app:chart]{the Appendix} gives
\begin{gather*}
(D_{12},D_{13},D_{14},D_{23},D_{24},D_{34})=\Bigl(0,\,\tfrac83h_1,\,\tfrac83h_3,\,\tfrac{8h_4}{3\gamma},\,\tfrac{8h_2}{3\gamma},\,\tfrac{16}9\Bigr),\\
(T_{12},T_{13},T_{14},T_{23},T_{24},T_{34})=\Bigl(0,\,\tfrac3{16},\,-\tfrac3{16},\,-\tfrac{3\gamma}{16},\,\tfrac{3\gamma}{16},\,-\tfrac{3\rho}{16}\Bigr),
\end{gather*}
and, since $q_1=(1,0)$, $q_2=(\frac12,\frac{\sqrt3}2)$ and $q_3=q_4=0$ there,
\begin{gather*}
\beta_{12}=0,\qquad \beta_{13}=-\beta_{14}=\frac{\gamma-2}{4\gamma}\Bigl(\frac1{\sqrt3},1\Bigr),\\
\beta_{23}=-\beta_{24}=\Bigl(-\frac{2\gamma-1}{2\sqrt3},0\Bigr),\qquad \beta_{34}=\frac{\rho}{2\gamma}\Bigl(\frac{1-2\gamma}{\sqrt3},1\Bigr).
\end{gather*}
Using $h_1+h_3=2-\gamma$ and $h_2+h_4=2\gamma-1$ we obtain
\[
\hat c_0=\tfrac3{32}(h_1+h_3)+\tfrac{3\gamma}{32}(h_2+h_4)+\tfrac{\rho^2}{16}=\tfrac{\rho^2}4,\qquad \hat b_0=\tfrac12(2-\gamma)\beta_{13}-\tfrac12(2\gamma-1)\beta_{23}-\tfrac\rho3\beta_{34},
\]
and
\[
G_0=\tfrac83(2-\gamma)\,\beta_{13}\beta_{13}^{\mathsf T}+\tfrac{8(2\gamma-1)}{3\gamma}\,\beta_{23}\beta_{23}^{\mathsf T}+\tfrac{16}9\,\beta_{34}\beta_{34}^{\mathsf T}-\tfrac4{\rho^2}\,\hat b_0\hat b_0^{\mathsf T}.
\]
This depends only on $\gamma$. Explicitly,
\[
G_0=\frac1{48\rho^2}\begin{pmatrix}3(-8\gamma^3+21\gamma^2-12\gamma+4)&\sqrt3\,(8\gamma^3-33\gamma^2+42\gamma-16)\\[2pt] \sqrt3\,(8\gamma^3-33\gamma^2+42\gamma-16)&\gamma^{-1}(-8\gamma^4+61\gamma^3-120\gamma^2+112\gamma-32)\end{pmatrix},
\]
and $\tr G_0=\frac14+\mu(\gamma)$, $\det G_0=\frac14\mu(\gamma)$. For example, at $\gamma=1$ we have $\hat b_0=\frac7{24}(\frac1{\sqrt3},-1)$ and
\[
G_0=\begin{pmatrix}\frac5{16}&\frac{\sqrt3}{48}\\[2pt] \frac{\sqrt3}{48}&\frac{13}{48}\end{pmatrix},
\]
with the eigenvalues $\frac14$ and $\frac13$. These computations were also carried out in computer algebra, and compared with the chart formulas evaluated at $b=10^{-15}$. The eigenvalues depend continuously on the matrix, so $\lmax(G)\to\max(\frac14,\mu(\gamma))$. Finally $\mu(\gamma)\le\frac13$, with equality if and only if $\gamma=1$, and $\mu(1)=\frac13>\frac14$.

(d) By Proposition~\ref{prop:majorant}(c), the smallest generalized eigenvalue of $(Q,K)$ at $q(z_b)$ is $1-\lmax(G)$. If $\gamma=1$, it tends to $\frac23$ by (c), and hence $\theta^*\le\frac23$. For $\alpha=0$ and $\gamma=1$ we have $a=1$ and $c=b$, so $q_3=-b\,q_1$ and $q_4=-b\,q_2$ with $|q_1|=|q_2|=1$. As in the proof of Corollary~C(ii), the reflection in the perpendicular bisector of $q_1q_2$ exchanges $q_1\leftrightarrow q_2$ and $q_3\leftrightarrow q_4$, so $q(z_b)$ is an isosceles trapezoid. The reflected configuration with the labels $1\leftrightarrow2$ and $3\leftrightarrow4$ exchanged is again $q(z_b)$, and it is a CC for the masses $(m_2,m_1,m_4,m_3)$. By the uniqueness of the masses in Lemma~\ref{lem:dziobekfn}(c), $(m_2,m_1,m_4,m_3)=t\,m$ for some $t>0$. Then $t^2=1$, so $m_1=m_2$ and $m_3=m_4$. Finally $\rho=1$ and $h_3^*=\frac12$, so $m_3/(b^3m_1)\to\frac34$ by (b).
\end{proof}

\begin{conjecture}\label{conj:sharp}
$\lmax(G)<\frac13$ at every convex CC. Consequently $Q\ge\frac23K$ at every convex CC, and by Proposition~\ref{prop:corner}(d) the constant $\frac23$ is optimal.
\end{conjecture}

The following floating-point observations support the conjecture; they are not part of any proof. At the corner, we maximized $\lmax(G)$ over $\gamma$ at the CCs with chart coordinates $(b,\alpha,\gamma)$, for fixed $b$ and $\alpha$. For $b=3\cdot10^{-2}$, $10^{-2}$ and $10^{-3}$ the maximum is $\frac13-c\,b^2$, attained at $\gamma=1+O(b)$, where $c>0$ depends on $\alpha$ and appears to converge as $b\to0$: for $|\alpha|\le0.3$ the three values of $c$ differ by less than $5\%$, while for $\alpha=-0.45$ they are $0.106$, $0.097$ and $0.092$. At $b=10^{-3}$, $c$ is $0.250$ for $\alpha=0$, and $0.232$--$0.233$, $0.180$, $0.092$ and $0.055$--$0.056$ for $\alpha=\pm0.15$, $\pm0.3$, $\pm0.45$ and $\pm0.4999$. Away from the corner, the largest value of $\lmax(G)$ at $18\,990$ sampled CCs of the direct region was $0.33127$. In a sample of $17\,516$ CCs of the chart region, the values approach $\frac13$ only as $b\to0$; compare Figure~\ref{fig:lmax}. At fixed $b$, a local maximization of $\lmax(G)$ ended at the boundary of $\cC$, where one of the masses tends to zero, with the values $0.33320$ for $b=0.05$, $0.33285$ for $b=0.1$, $0.33164$ for $b=0.2$, $0.32847$ for $b=0.4$ and $0.32429$ for $b=0.8$. These are limits of values at convex CCs and lower estimates of the suprema at fixed $b$. They have the form $\frac13-c\,b^2$ with $c$ increasing from $0.014$ at $b=0.8$ to $0.052$ at $b=0.05$, close to the values $0.055$--$0.056$ found at the corner for $\alpha=\pm0.4999$. Since $\lmax(G_0)=\frac13$ along $\gamma_*=1$, a proof of the conjecture near the corner has to use the expansion of $\lmax(G)$ to second order in $b$.

\subsection{Open questions}
\begin{enumerate}[label=\textup{(\arabic*)},leftmargin=2em]
\item \emph{The optimal constant.} Prove Conjecture~\ref{conj:sharp}.
\item \emph{A proof without computer assistance.} By Proposition~\ref{prop:majorant}(c) and the argument of Section~\ref{sec:proofs}, uniqueness follows as soon as $1$ is not an eigenvalue of $G$ at any convex CC, while numerically $\lmax(G)<\frac13$. The margin is large, but we do not know a conceptual reason for it.
\item \emph{Dziobek configurations.} By Remark~\ref{rem:identity}(ii), $Q=K+\sigma|\sum_lA_lv_l|^2$ for Dziobek configurations of $d+2$ bodies in $\R^d$. Is there an analogue of Theorem~B for some class of Dziobek CCs?
\item \emph{Other homogeneous potentials.} For the potential $\sum_{i<j}m_im_jr_{ij}^{-a}$ with $a>0$, the same computation gives $\kappa_e=a(a+2)m_im_jr_e^{-a-2}$ and $w_e=a\,r_e^{-a-2}-\lambda'$. The proof of Lemma~\ref{lem:dziobek} again gives $\sigma<0$, and $D_e=|\sigma|/\kappa_e$ is again independent of the masses, so Propositions~\ref{prop:identity} and~\ref{prop:majorant} carry over. An analogue of Theorem~A would need a new computation, to prove an analogue of Theorem~B. Given that, Lemma~\ref{lem:collinear} and the base case with equal masses carry over: the computation in the proof of Lemma~\ref{lem:collinear} uses only that $r^{-a-2}$ is decreasing, and \cite[Theorem~1]{AFS08} holds for these potentials. We have not attempted this.
\item \emph{Concave CCs.} Proposition~\ref{prop:majorant}(c) applies to concave CCs as well: a concave CC is degenerate if and only if $1$ is an eigenvalue of its matrix $G$. Degenerate concave CCs exist \cite{Rob25,LX25,LPRX26}. It would be interesting to describe the set of masses for which they occur.
\end{enumerate}

\section*{Appendix. Formulas of the blow-up chart}\phantomsection\label{app:chart}
This appendix lists the formulas used in the chart $(b,\alpha,\gamma,\xi)$ of Section~\ref{sec:chart}. Recall that $a=1+b\alpha$, $c=b\gamma$, $x=\frac12+b\xi$ and $s=\sqrt{1-x^2}$, and let $h_i$, $d_e$, $\rho^2$, $\he_e$, $\hat\delta$ and $\hat P$ be as in Section~\ref{sec:chart}. For $e\ne34$ put $R_e=1+b\,d_e$, $r_e=\sqrt{R_e}$ and $s_e=1/(R_er_e)$. Put $\rho=\sqrt{\rho^2}$ and $R_{34}=b^2\rho^2$, so that $r_{34}=b\rho$ and $s_{34}=b^{-3}\rho^{-3}$ for $b>0$.

\subsection*{The quantities \texorpdfstring{$w_e$}{w\_e}}
Lemma~\ref{lem:dziobekfn}(a) gives $w_{12}=b^5\hw_{12}$, $w_e=b\,\hw_e$ for $e\in\{13,14,23,24\}$ and $w_{34}=b^{-3}\hw_{34}$, where
\begin{gather*}
\hw_{12}=\frac{\he_{13}\he_{24}}{\hat\delta},\qquad
\hw_{13}=-\frac{\he_{13}\,(\he_{34}+b^4\he_{13})}{\hat\delta},\qquad
\hw_{24}=-\frac{\he_{24}\,(\he_{34}+b^4\he_{24})}{\hat\delta},\\
\hw_{14}=\he_{14}+b^4\hw_{12},\qquad
\hw_{23}=\he_{23}+b^4\hw_{12},\qquad
\hw_{34}=\frac{(\he_{34}+b^4\he_{13})(\he_{34}+b^4\he_{24})}{\hat\delta}.
\end{gather*}

\subsection*{Areas}
We have $A_1=b\hA_1$ and $A_2=b\hA_2$, where
\[
\hA_1=\tfrac s2\,(a+c),\qquad \hA_2=-\tfrac s2\,\gamma\,(1+b),\qquad\text{and}\qquad A_3=\tfrac s2\,(a+c),\qquad A_4=-\tfrac s2\,a\,(1+b).
\]

\subsection*{The coefficients \texorpdfstring{$D_e$}{D\_e}}
Inserting these expressions into \eqref{eq:De}, and using $w_{34}/s_{34}=\rho^3\hw_{34}$, we get
\begin{gather*}
D_{12}=-\frac{b^3\hw_{12}}{3s_{12}\hA_1\hA_2},\qquad D_{13}=-\frac{\hw_{13}}{3s_{13}\hA_1A_3},\qquad D_{14}=-\frac{\hw_{14}}{3s_{14}\hA_1A_4},\\
D_{23}=-\frac{\hw_{23}}{3s_{23}\hA_2A_3},\qquad D_{24}=-\frac{\hw_{24}}{3s_{24}\hA_2A_4},\qquad D_{34}=-\frac{\rho^3\hw_{34}}{3A_3A_4}.
\end{gather*}

\subsection*{The self-stress}
The rescaled self-stress $T_e=\tau_e/b$, with $\tau_e=A_iA_jr_e$ as in Lemma~\ref{lem:rigid}, is
\begin{gather*}
T_{12}=b\,\hA_1\hA_2\,r_{12},\qquad T_{13}=\hA_1A_3\,r_{13},\qquad T_{14}=\hA_1A_4\,r_{14},\\
T_{23}=\hA_2A_3\,r_{23},\qquad T_{24}=\hA_2A_4\,r_{24},\qquad T_{34}=A_3A_4\,\rho.
\end{gather*}

\subsection*{The vectors \texorpdfstring{$\beta_e$}{beta\_e}}
The vectors $\beta_e$ of Lemma~\ref{lem:beta} are not rescaled. With $q_1=(1,0)$, $q_2=a\,(x,s)$, $q_3=(-b,0)$ and $q_4=-c\,(x,s)$, they are $\beta_e=-\sum_{l\notin e}C_{e,l}\,q_l$, where
\begin{align*}
C_{12,3}&=\frac{r_{12}\,(R_{14}+R_{24}-R_{12})}{8A_3}, & C_{12,4}&=\frac{r_{12}\,(R_{13}+R_{23}-R_{12})}{8A_4},\\
C_{13,2}&=\frac{r_{13}\,(d_{14}-d_{13}+b\rho^2)}{8\hA_2}, & C_{13,4}&=\frac{r_{13}\,(R_{12}+R_{23}-R_{13})}{8A_4},\\
C_{14,2}&=\frac{r_{14}\,(d_{13}-d_{14}+b\rho^2)}{8\hA_2}, & C_{14,3}&=\frac{r_{14}\,(R_{12}+R_{24}-R_{14})}{8A_3},\\
C_{23,1}&=\frac{r_{23}\,(d_{24}-d_{23}+b\rho^2)}{8\hA_1}, & C_{23,4}&=\frac{r_{23}\,(R_{12}+R_{13}-R_{23})}{8A_4},\\
C_{24,1}&=\frac{r_{24}\,(d_{23}-d_{24}+b\rho^2)}{8\hA_1}, & C_{24,3}&=\frac{r_{24}\,(R_{12}+R_{14}-R_{24})}{8A_3},\\
C_{34,1}&=\frac{\rho\,(R_{23}+R_{24}-R_{34})}{8\hA_1}, & C_{34,2}&=\frac{\rho\,(R_{13}+R_{14}-R_{34})}{8\hA_2}.
\end{align*}
These are the coefficients $C_{e,l}=r_eN_{e,l}/(8A_l)$ of Lemma~\ref{lem:beta}. For the four coefficients with $l\in\{1,2\}$ and $e\ne34$ we used
\[
N_{13,2}=R_{14}+R_{34}-R_{13}=b\,(d_{14}-d_{13}+b\rho^2),\qquad N_{14,2}=b\,(d_{13}-d_{14}+b\rho^2),
\]
\[
N_{23,1}=b\,(d_{24}-d_{23}+b\rho^2),\qquad N_{24,1}=b\,(d_{23}-d_{24}+b\rho^2),
\]
and for $e=34$ we used $r_{34}=b\rho$. In each case the factor $b$ cancels the factor $b$ of $A_1$ or $A_2$.

\subsection*{Analyticity at \texorpdfstring{$b=0$}{b=0}}
At a point with $b=0$ and $\gamma>0$ we have $x=\frac12$, $s=\frac{\sqrt3}2$, $R_e=1$ for $e\ne34$, $\rho^2=\gamma^2-\gamma+1>0$, $\hA_1=\frac{\sqrt3}4$, $\hA_2=-\frac{\sqrt3}4\gamma$, $A_3=-A_4=\frac{\sqrt3}4$ and $\hat\delta=\rho^{-3}$. So every denominator above is nonzero and every square root has a positive argument, and all these quantities are real-analytic in a neighbourhood of the point.

These are the formulas used in the chart computation, and check~(3) of Section~\ref{sec:results} compares them with the direct formulas in computer algebra.

\section*{Data and code availability}
The programs, the certificate files, the logs and the Lean formalization are available at
\begin{center}
\url{https://github.com/tejasvi/lean4body}\\
release \texttt{v1.0}, commit \texttt{58ac0fbf4d66},\\
archived at \url{https://doi.org/10.5281/zenodo.23004297}.
\end{center}
The repository contains the program of Section~\ref{sec:procedure} with the certificate files and the logs of the runs in Table~\ref{tab:runs}; the scripts of the checks of Section~\ref{sec:results}, of Figure~\ref{fig:lmax}, of the computer-algebra computation in the proof of Proposition~\ref{prop:corner} and of the observations after Conjecture~\ref{conj:sharp}; the second implementation of Section~\ref{sec:indep}, with its specification, the record of its development and its logs; and the Lean formalization of Section~\ref{sec:lean}. The computations use Python~3.14.4 with \texttt{python-flint}~0.9.0 (Arb), \texttt{mpmath}~1.3.0, \texttt{sympy}~1.14.0 and \texttt{numpy}~2.5.3, and the formalization uses Lean~4.35.0-rc3 and Mathlib at the tag \texttt{v4.35.0-rc3}. The file \texttt{README.md} of the repository describes the files, gives the SHA-256 hashes of the programs and the certificate files, and gives the commands that repeat the computations and check the formal proof.

\section*{Use of AI tools}
Generative AI tools were used to find and prove the results, to write both programs of Section~\ref{sec:cap} and the Lean formalization, and to draft the text.

\begin{thebibliography}{CCLM15}

\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[ACS12]{ACS12}
A.~Albouy, H.~E. Cabral and A.~A. Santos, \emph{Some problems on the classical $n$-body problem}, Celest. Mech. Dyn. Astron. \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. A \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. \textbf{176} (2012), 535--588.

\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.

\bibitem[CCLP19]{CCLP19}
M.~Corbera, J.~M. Cors, J.~Llibre and E.~P\'erez-Chavela, \emph{Trapezoid central configurations}, Appl. Math. Comput. \textbf{346} (2019), 127--142.

\bibitem[CCR18]{CCR18}
M.~Corbera, J.~M. Cors and G.~E. Roberts, \emph{A four-body convex central configuration with perpendicular diagonals is necessarily a kite}, Qual. Theory Dyn. Syst. \textbf{17} (2018), 367--374.

\bibitem[CCR19]{CCR19}
M.~Corbera, J.~M. Cors and G.~E. Roberts, \emph{Classifying four-body convex central configurations}, Celest. Mech. Dyn. Astron. \textbf{131} (2019), Paper No.~34.

\bibitem[CR12]{CR12}
J.~M. Cors and G.~E. Roberts, \emph{Four-body co-circular central configurations}, Nonlinearity \textbf{25} (2012), 343--370.

\bibitem[Dia26]{Dia26}
T.~Dias, \emph{Brehm--Wintner--Conley dimension, Pl\"ucker coordinates, and generalized Dziobek--Williams equations for central configurations}, arXiv:2608.07771 (2026).

\bibitem[Dzi00]{Dzi00}
O.~Dziobek, \emph{\"Uber einen merkw\"urdigen Fall des Vielk\"orperproblems}, Astron. Nachr. \textbf{152} (1900), 33--46.

\bibitem[FLM17]{FLM17}
A.~C. Fernandes, J.~Llibre and L.~F. Mello, \emph{Convex central configurations of the $4$-body problem with two pairs of equal adjacent masses}, Arch. Ration. Mech. Anal. \textbf{226} (2017), 303--320.

\bibitem[Ham02]{Ham02}
M.~Hampton, \emph{Concave central configurations in the four-body problem}, PhD thesis, University of Washington, 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.

\bibitem[Joh17]{Joh17}
F.~Johansson, \emph{Arb: efficient arbitrary-precision midpoint-radius interval arithmetic}, IEEE Trans. Comput. \textbf{66} (2017), 1281--1292.

\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[LX25]{LX25}
Y.~Liu and Z.~Xie, \emph{Symmetric central configurations in the concave $4$-body problem with two pairs of equal masses}, arXiv:2510.25638 (2025).

\bibitem[LS02]{LS02}
Y.~Long and S.~Sun, \emph{Four-body central configurations with some equal masses}, Arch. Ration. Mech. Anal. \textbf{162} (2002), 25--44.

\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[Moe01]{Moe01}
R.~Moeckel, \emph{Generic finiteness for Dziobek configurations}, Trans. Amer. Math. Soc. \textbf{353} (2001), 4673--4686.

\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[MKC09]{MKC09}
R.~E. Moore, R.~B. Kearfott and M.~J. Cloud, \emph{Introduction to Interval Analysis}, SIAM, 2009.

\bibitem[Pac87]{Pac87}
F.~Pacella, \emph{Central configurations of the $N$-body problem via equivariant Morse theory}, Arch. Ration. Mech. Anal. \textbf{97} (1987), 59--74.

\bibitem[Pal73]{PalI}
J.~I. Palmore, \emph{Classifying relative equilibria.~I}, Bull. Amer. Math. Soc. \textbf{79} (1973), 904--908.

\bibitem[Pal75]{PalII}
J.~I. Palmore, \emph{Classifying relative equilibria.~II}, Bull. Amer. Math. Soc. \textbf{81} (1975), 489--491.

\bibitem[PCS07]{PCS07}
E.~P\'erez-Chavela and M.~Santoprete, \emph{Convex four-body central configurations with some equal masses}, Arch. Ration. Mech. Anal. \textbf{185} (2007), 481--494.

\bibitem[Rob25]{Rob25}
G.~E. Roberts, \emph{On kite central configurations}, Nonlinearity \textbf{38} (2025), 075001.

\bibitem[San21a]{San21a}
M.~Santoprete, \emph{On the uniqueness of co-circular four-body central configurations}, Arch. Ration. Mech. Anal. \textbf{240} (2021), 971--985.

\bibitem[San21b]{San21b}
M.~Santoprete, \emph{On the uniqueness of trapezoidal four-body central configurations}, Nonlinearity \textbf{34} (2021), 424--437.

\bibitem[San26]{San26}
M.~Santoprete, \emph{The Hessian of planar central configurations in pair space: decomposition, Morse index and symmetry reduction}, arXiv:2609.01857 (2026).

\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[Sma70]{Sma70}
S.~Smale, \emph{Topology and mechanics.~II. The planar $n$-body problem}, Invent. Math. \textbf{11} (1970), 45--64.

\bibitem[SXY23]{SXY23}
S.~Sun, Z.~Xie and P.~You, \emph{On the uniqueness of convex central configurations in the planar $4$-body problem}, Regul. Chaotic Dyn. \textbf{28} (2023), 512--532.

\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[Tuc11]{Tuc11}
W.~Tucker, \emph{Validated Numerics: A Short Introduction to Rigorous Computations}, Princeton Univ. Press, 2011.

\bibitem[Xia04]{Xia04}
Z.~Xia, \emph{Convex central configurations for the $n$-body problem}, J. Differential Equations \textbf{200} (2004), 185--190.

\bibitem[Xie12]{Xie12}
Z.~Xie, \emph{Isosceles trapezoid central configurations of the Newtonian four-body problem}, Proc. Roy. Soc. Edinburgh Sect. A \textbf{142} (2012), 665--672.

\end{thebibliography}

\end{document}