\documentclass[11pt,a4paper]{article}
\usepackage[margin=27mm]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,longtable,array}
\usepackage[T1]{fontenc}
\usepackage{lmodern,microtype}
\usepackage{xcolor}
\usepackage{listings}
\usepackage[colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black]{hyperref}
\def\UrlBreaks{\do\/\do\.\do\_}
\usepackage{enumitem}
\setlist{itemsep=3pt,topsep=5pt}
\setlength{\emergencystretch}{2em}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
\newcommand{\C}{\mathbb C}
\newcommand{\R}{\mathbb R}
\newcommand{\calR}{\mathcal R}
\newcommand{\norm}[1]{\lvert #1\rvert}
\newcommand{\code}[1]{\nolinkurl{#1}}
\lstset{basicstyle=\ttfamily\footnotesize,columns=fullflexible,breaklines=true,keepspaces=true,frame=single,rulecolor=\color{black!20},xleftmargin=3pt,xrightmargin=3pt}

\newcommand{\eps}{\varepsilon}
\newcommand{\ii}{\mathrm i}
\newcommand{\asym}{\asymp}
\title{Finiteness of Planar Central Configurations\\for Five Positive Masses}
\author{Chih-Yao Wu\thanks{Correspondence: \href{mailto:andersonwu2000@gmail.com}{andersonwu2000@gmail.com}. AI agents carried out the mathematical development and manuscript preparation under the author's coordination. An independent human expert review of the complete argument has not yet been completed. See Section~\ref{sec:verification} and Appendix~\ref{app:leanmap} for contributions and formal verification.}}
\date{October 21, 2026}
\begin{document}
\maketitle
\begin{abstract}
We prove that, for any five positive masses, there are finitely many planar Newtonian central configurations up to translations, rotations, and positive scaling. Building on the singular-diagram framework of Albouy and Kaloshin, we treat the exceptional masses left open by their finiteness theorem. The proof retains a lower bound for the physical potential after passing to the complex algebraic equations. On each fixed potential level, energy estimates, torque identities, and local response calculations control the possible degenerations. A polynomial selection argument then yields finiteness. The exceptional local calculations and their algebraic certificates are given explicitly. A separate Lean development accompanies the proof.
\end{abstract}
\tableofcontents
\newpage

\section{Introduction}
Fix labelled masses $m_1,\ldots,m_5>0$. A planar central configuration consists of distinct $q_i\in\R^2$ satisfying
\begin{equation}\label{eq:physical}
\lambda(q_i-c)=\sum_{j\ne i}m_j\frac{q_i-q_j}{|q_i-q_j|^3}.
\end{equation}
Here $c\in\mathbb R^2$ is the center and $\lambda\in\mathbb R$ is the multiplier; the equations will imply that $c$ is the mass center. A proper similarity is $q\mapsto sOq+t$, with $s>0$ and $O\in\mathrm{SO}(2)$. The following statement includes repeated masses and collinear configurations. Reflection and label permutations are not part of this equivalence relation.

This is the planar five-body instance of the finiteness question in Smale's sixth problem~\cite{Smale}. Hampton and Moeckel proved finiteness for four positive masses~\cite{HM}. For five bodies, Albouy and Kaloshin proved finiteness outside an explicitly specified algebraic subset of codimension two in the positive mass space~\cite{AK}. Their method classifies the singular limits that could arise from an infinite family and derives restrictions on the masses from those limits. The exceptional set records the masses for which that argument leaves finiteness open.

The theorem below removes this mass restriction. The main issue is to retain physical information while analyzing complex degenerations. Roberts' continuum, discussed in Section~\ref{sec:algebra}, illustrates why this distinction matters. We keep the potential fixed and use a lower bound that survives complexification.

\begin{theorem}\label{thm:main}
For every fixed labelled mass vector $(m_1,\ldots,m_5)\in(0,\infty)^5$, the planar Newtonian central configurations have finitely many proper-similarity classes.
\end{theorem}
The classification used in Section~\ref{sec:entrance} is AK's sixteen-diagram list, obtained through the matrix enumeration and order refinement developed by Chang and Chen~\cite{CCI,CCII} and applied to five bodies in Chang's thesis~\cite{ChangThesis}. We use that classification as a cited result and supply the subsequent local arguments for arbitrary positive masses. The pair--triple degeneration D2 requires a response calculation and a classification of its exceptional eigenvalues; the butterfly degeneration D6 requires a fourth-order torque calculation. D5 supplies the product decay used in the global argument. For D8 and D9, compatibility and energy estimates give the required exclusions. Section~\ref{sec:local} summarizes the remaining cases and the order of their treatment.

Two related developments help place the result in context. Moczurad and Zgliczy\'nski give computer-assisted exact counts for several specified five-body mass vectors that are exceptional for earlier finiteness results~\cite{MZ}. Here the conclusion is finiteness for every positive mass vector, without an exact count. Yu and Zhu prove finiteness of stationary configurations for five vortices with vorticities of one sign~\cite{YZ}; their result concerns the vortex equations, rather than the Newtonian force law considered here.

Contemporaneous preprints by Tomar~\cite{Tomar} and Chen and Tong~\cite{ChenTong} also present proofs of finiteness for all five positive masses. Tomar supplies a Lean formalization and computational certificates. The present argument was developed independently of these works. Its organization centers on the physical potential bound, local control on each fixed potential level, and the polynomial selection argument described below.

\subsection{Outline of the argument}
The proof first normalizes the configurations and establishes a lower bound for their potential. We then pass to complex polynomial equations while retaining this numerical bound. Only finitely many potential values occur, so it suffices to work at one fixed value.

On each such level, finiteness reduces to controlling ten products of squared distances, called four-products. If one has infinite image, algebraic geometry supplies a sequence along which its modulus diverges. After rescaling, this sequence has one of sixteen singular diagrams. The local arguments exclude all but a collapsing-triple case, or show that the selected product cannot diverge.

The collapsing triple requires a different conclusion: a fixed product, chosen from the masses alone, tends to zero. A second polynomial selection turns this decay into a contradiction. Sections~\ref{sec:products}--\ref{sec:selection} establish the algebraic mechanism; Sections~\ref{sec:entrance}--\ref{sec:local} specify the local statement; the remaining sections prove it diagram by diagram.

\subsection{Conventions}
All labels remain distinct even if some masses coincide. Complex inertia is bilinear, not Hermitian. Every inverse-distance sheet is retained after complexification. For complex sequences, $f=O(g)$ and $f=o(g)$ refer to moduli, and $f\asym g$ means two-sided comparability of moduli. A subsequence is always common to the finitely many quantities being discussed. After complexification, physical information is carried by the fixed real potential value and its lower bound. Local coordinates and inverse distances may be complex. We reserve $M,S,U,I,u$ for the total mass, mass-pair sum, potential, inertia, and fixed potential value; $R$ denotes the balanced scale. Mass and coordinate symbols introduced within a local case are used only in that case.
\section{Normalization and the physical invariant}\label{sec:normalize}
Write
\[
 M=\sum_i m_i,\qquad S=\sum_{i<j}m_im_j,\qquad
 U(q)=\sum_{i<j}\frac{m_im_j}{\norm{q_i-q_j}}.
\]

\begin{lemma}\label{lem:normalization}
A solution of \eqref{eq:physical} has positive multiplier, has $c=M^{-1}\sum_i m_iq_i$, and is properly similar to a solution with center zero and multiplier one.
\end{lemma}
\begin{proof}
Multiply each force equation by $m_i(q_i-c)$ using the Euclidean inner product and sum. Pairing the terms for $i,j$ gives
\[
 \lambda\sum_i m_i\norm{q_i-c}^2=U(q)>0.
\]
The inertia is positive because the points are distinct. Hence $\lambda>0$. The mass-weighted sum of the force equations is $\lambda\sum_i m_i(q_i-c)=0$, proving the center assertion. Translate by $-c$ and multiply positions by $\lambda^{1/3}$. The resulting multiplier is one, since scaling positions by $s$ divides the multiplier by $s^3$.
\end{proof}

For normalized real configurations put $I=\sum_i m_i\norm{q_i}^2$. The same calculation gives $U=I$.

\begin{lemma}[Physical potential floor]\label{lem:floor}
If $u$ is the potential of a normalized physical configuration, then
\begin{equation}\label{eq:floor}
 u>0,\qquad M u^3\ge S^3.
\end{equation}
\end{lemma}
\begin{proof}
For positive $r_e$ and nonnegative weights $w_e$, H\"older's inequality gives
\[
 \left(\sum_e w_e\right)^3
 \le\left(\sum_e w_er_e^2\right)
       \left(\sum_e\frac{w_e}{r_e}\right)^2.
\]
Take $e=\{i,j\}$, $w_e=m_im_j$, and $r_e=\norm{q_i-q_j}$. Centering gives
\[
 \sum_{i<j}m_im_jr_{ij}^2=MI,
\]
so $S^3\le MIU^2=MU^3$. Positivity of $U$ is immediate. The displayed inequality is ordinary weighted H\"older, applied to $w_e=(w_er_e^2)^{1/3}(w_e/r_e)^{2/3}$.
\end{proof}

Call a real number $u$ \emph{physically admissible} when it satisfies \eqref{eq:floor}. This condition will restrict the potential values of the complex level sets. Their points and singular limits may have complex coordinates and arbitrary inverse-distance sheets; existence of a physical representative is a separate question.

\section{The complex algebraic model and its finite invariants}\label{sec:algebra}
Use complex coordinates $z_i=x_i+\mathrm{i}y_i$, $w_i=x_i-\mathrm{i}y_i$. After complexification, $z$ and $w$ are independent. Introduce symmetric variables $\delta_{ij}$ for $i\ne j$, and set
\[
 d_{ij}=(z_i-z_j)(w_i-w_j).
\]
The normalized equations are
\begin{align}
 z_i&=\sum_{j\ne i}m_j\delta_{ij}^3(z_i-z_j),&
 w_i&=\sum_{j\ne i}m_j\delta_{ij}^3(w_i-w_j),\label{eq:complexforce}\\
 \delta_{ij}^2d_{ij}&=1.&&\label{eq:metric}
\end{align}
The physical branch has $w_i=\overline z_i$ and $\delta_{ij}=1/\norm{q_i-q_j}>0$. The complex equations retain every signed branch. In particular, $d_{ij}$ and $\delta_{ij}$ never vanish.

The weighted sums of \eqref{eq:complexforce} show $\sum_i m_iz_i=\sum_i m_iw_i=0$. Rotation complexifies to
\[
 (z,w,\delta)\longmapsto(az,a^{-1}w,\delta),\qquad a\in\C^*.
\]
Fix the gauge $z_1-z_2=w_1-w_2$, equivalently $y_1=y_2$. Because $d_{12}\ne0$, the equation
\[
 a^2=\frac{w_1-w_2}{z_1-z_2}
\]
has precisely two nonzero solutions. Thus this gauge meets each complex rotation orbit in finitely many points, including at collinear configurations. Denote the resulting affine algebraic set by $X_m$.

On the complex solution set define
\[
 U=\sum_{i<j}m_im_j\delta_{ij},\qquad
 I=\sum_i m_iz_iw_i=\sum_i m_i(x_i^2+y_i^2).
\]
These are bilinear algebraic expressions; no complex conjugation is used in $I$.

\begin{lemma}[Finite potential values]\label{lem:values}
The normalized complex solution set has only finitely many values of $U$.
\end{lemma}
\begin{proof}
Let $A$ be the coordinate ring of the normalized complex solution set. Fix a minimal prime $\mathfrak p$ of $A$ and write $K=\operatorname{Frac}(A/\mathfrak p)$. All force and metric identities hold in $K$, and the masses are fixed elements of $\mathbb C$. We first show that every $\mathbb C$-derivation $D:K\to K$ annihilates $U$.

Write $x_i=(z_i+w_i)/2$ and $y_i=(z_i-w_i)/(2\ii)$ in $K$. The pairwise symmetrization used in the real virial identity is bilinear and therefore also applies in $K$, giving $U=I$. Differentiating \eqref{eq:metric} gives
\[
 D\delta_{ij}=-\delta_{ij}^3\bigl((x_i-x_j)D(x_i-x_j)
                     +(y_i-y_j)D(y_i-y_j)\bigr).
\]
Summing these derivatives with weights $m_im_j$ and grouping by body gives
\begin{align*}
 DU&=-\sum_i m_i\left[
 Dx_i\sum_{j\ne i}m_j\delta_{ij}^3(x_i-x_j)
 +Dy_i\sum_{j\ne i}m_j\delta_{ij}^3(y_i-y_j)\right]\\
 &=-\sum_i m_i(x_iDx_i+y_iDy_i)=-\tfrac12 DI.
\end{align*}
Combined with $DU=DI$, this implies $3DU=0$ and hence $DU=0$.

To conclude that $U$ is constant, suppose instead that it is transcendental over $\mathbb C$. It can then be included in a transcendence basis $U,t_2,\ldots,t_d$ of the finitely generated field $K/\mathbb C$. The derivation $\partial/\partial U$ on $\mathbb C(U,t_2,\ldots,t_d)$ extends to $K$, since $K$ is a finite separable extension in characteristic zero. This gives $DU=1$, a contradiction. Thus $U$ is algebraic over the algebraically closed field $\mathbb C$, and equals a scalar on this component.

There are finitely many minimal primes because $A$ is Noetherian. Every complex point lies on at least one of their components, so its potential equals one of these finitely many scalars. Embedded components and nilpotents do not add values at complex points.
\end{proof}


For a fixed scalar $u\in\C$ let
\[
 X_{m,u}=\{x\in X_m:U(x)=u\}.
\]
It suffices to prove that $X_{m,u}$ is finite for every physically admissible $u$. This does not claim finiteness of the whole signed-complex set $X_m$ at other potential values.

\begin{remark}[Why the branch restriction matters]
Roberts' continuum~\cite{Roberts} has mass ratios $(4,4,4,4,-1)$, with the negative mass at the center. Albouy--Kaloshin~\cite[Section~2, p.~543]{AK} change the central mass sign and the four incident signed distances, obtaining positive mass ratios $(4,4,4,4,1)$ but negative central inverse distances. This is a continuum in the signed algebraic system, not in the physical positive-distance branch. The distinction is therefore essential. In AK's normalization $U=1$, $M=17/8$, and $S=7/4$ for the modified family, so $MU^3=17/8<343/64=S^3$: its level also fails the physical floor used here.
\end{remark}

\section{Four-products and finite distance data}\label{sec:products}
Let $\mathcal E$ be the ten unordered pairs of labels. If $e=\{i,j\}$ and its complementary triple is $T=\{k,l,r\}$, set
\begin{equation}\label{eq:fourproduct}
 Q_e=d_{ij}d_{kl}d_{kr}d_{lr}.
\end{equation}
These are the original four-products of squared distances. Each is a polynomial that is nowhere zero on $X_m$.

\begin{lemma}\label{lem:recovery}
If every $Q_e$ has finite image on a subset $Y\subseteq X_m$, then $Y$ is finite.
\end{lemma}
\begin{proof}
For each edge $e$, direct counting of the exponents of every squared distance gives
\begin{equation}\label{eq:recovery}
 d_e^8\prod_{f\in\mathcal E}Q_f
 =\left(\prod_{\substack{f\in\mathcal E\\f\cap e=\varnothing}}Q_f\right)^4.
\end{equation}
The denominator $\prod_fQ_f$ never vanishes. Therefore $d_e^8$, and hence $d_e$, has finite image. There are at most eight choices over each eighth-power value.

It remains to reconstruct gauged coordinates from finite distance data. Put $h=x_1-x_2\ne0$; the gauge gives $h^2=d_{12}$. For each $k$,
\[
 x_1-x_k=\frac{d_{1k}+d_{12}-d_{2k}}{2h},\qquad
 (y_1-y_k)^2=d_{1k}-(x_1-x_k)^2.
\]
There are finitely many choices for all differences. Centering fixes the translation, and each equation $\delta_{ij}^2d_{ij}=1$ leaves at most two inverse-distance choices. No noncollinearity or generic rank assumption is needed.
\end{proof}

\section{Two polynomial selections}\label{sec:selection}
We isolate the global algebraic mechanism. A polynomial with bounded image on a complex affine algebraic set has finite image: its image is constructible in $\C$, and an infinite constructible subset of $\C$ contains a cofinite subset. This is the one-dimensional consequence of Chevalley's constructibility theorem; reducibility of the affine set causes no difficulty.

\begin{proposition}[Two-selection principle]\label{prop:selection}
Let $X$ be a complex affine algebraic set and $f_1,\ldots,f_N$ polynomials. Suppose finite images of all $f_j$ imply finiteness of $X$. Fix $A\subseteq\{1,\ldots,N\}$ and write $P=\prod_{j\in A}f_j$. Assume:
\begin{enumerate}
\item $f_j$ is nowhere zero on $X$ for every $j\in A$;
\item whenever $x_k\in X$ and $\norm{f_j(x_k)}\to\infty$ for any $j$, some subsequence satisfies $P(x_{k_\nu})\to0$.
\end{enumerate}
Then $X$ is finite.
\end{proposition}
\begin{proof}
If $X$ were infinite, at least one $f_j$ would have infinite image. Its image is unbounded, so choose $x_k$ with $\norm{f_j(x_k)}\to\infty$. The decay hypothesis gives $P(x_{k_\nu})\to0$. Since $P$ is nowhere zero, its image cannot be finite: a finite set of nonzero complex numbers is closed and excludes zero.

Select a second sequence $y_k\in X$ with $\norm{P(y_k)}\to\infty$. Some factor $f_j$, $j\in A$, is unbounded along this sequence; passing to a subsequence makes its modulus tend to infinity. Apply the same decay hypothesis again. Along a further subsequence $P$ tends to zero, whereas its modulus still tends to infinity. This contradiction proves the result. If $A$ is empty, $P=1$, and already the first decay conclusion is impossible.
\end{proof}

The two selected sequences need not lie on a common irreducible curve. They do lie on the same affine set $X$, with the same scalar $u$, masses, and product $P$. The original factor selected at the second step need not be the factor selected at the first.

In our application $X=X_{m,u}$ and $f_j=Q_e$. Lemma~\ref{lem:recovery} supplies the finite-data hypothesis. All that remains is to construct a mass-dependent product and prove the precise subsequence-decay assertion.


\section{Balanced extraction and diagram classification}\label{sec:entrance}

To analyze a divergent four-product, we use the singular-diagram framework of Albouy and Kaloshin~\cite{AK}. We rescale the two complex coordinate directions to a common size and extract a limit. Circles record coordinates that remain nonzero at the leading scale; strokes record such force terms. The precise normalization and estimates follow below. The sixteen diagram types are those of AK's Figure~11. We obtain their finite coverage through the matrix enumeration and order refinement of Chang and Chen, as recorded in~\cite[Section~10, pp.~65--66]{ChangThesis}.

\begin{theorem}[Sixteen-diagram classification]\label{thm:classification}
Fix five positive masses. Consider a singular balanced sequence of solutions of the signed-complex, multiplier-one force and metric equations. After passing to a subsequence, applying one common relabeling to coordinates and masses, and possibly interchanging $z$ and $w$, its diagram is one of the sixteen types D1--D16 in AK's Figure~11, described in the table below. Strokes and circles have the asymptotic meanings defined in Section~\ref{subsec:extraction}. The classification includes repeated masses.
\end{theorem}

\paragraph{Source and applicability.}
We use the classification established in~\cite[Section~10]{ChangThesis}.
Encode each color by a symmetric binary matrix: diagonal entries record circles and off-diagonal entries record strokes. The necessary analytic estimates and coloring rules originate in AK and are collected in Section~2 of~\cite{ChangThesis}; Sections~3--4 develop matrix rules and order criteria from them. Algorithm~I, including the rules implemented in Appendix~I, leaves the twenty diagram types in Figure~9 of that thesis, modulo a common permutation and color exchange. Algorithm~II refines the possible orders of the coordinates and differences. As reported at the start of Section~10, it excludes the four candidates $9,11,13,17$, leaving exactly AK's sixteen types. The algorithms and their implementations are given in Sections~6--7 and Appendices~I--II. This is the five-body application of the matrix and order methods.

The hypotheses hold for our sequences. The reciprocal rescaling below preserves both force equations and the metric equations, and its two normalized color vectors have nonzero limits. The masses are fixed and positive; every nonempty cluster therefore has nonzero total mass, and $m_i^3+m_j^3\ne0$. Potential values are bounded by Lemma~\ref{lem:values}, as required by the bounded-potential coloring rules. These conditions hold also when masses coincide. Finally, the survivor correspondence with AK's Figure~11 is stated in~\cite[Section~10]{ChangThesis}; the explicit numbering correspondence is reproduced in Appendix~\ref{app:leanmap}.


\begin{remark}[Classification and local analysis]\label{rem:classification}
The classification supplies the list of possible limits. The local conclusions needed for finiteness are proved below, including the fixed-potential treatment of D9 in Section~\ref{sec:D9}. Appendix~\ref{app:leanmap} describes the corresponding formal classification and the analytic rules it uses.
\end{remark}

\subsection{Extraction, scales, and basic estimates}\label{subsec:extraction}

For $i\neq j$ set
\[
 Z_{ij}=\delta_{ij}^3(z_i-z_j),\qquad W_{ij}=\delta_{ij}^3(w_i-w_j),\qquad r_{ij}=\delta_{ij}^{-1}.
\]
Let $N_z$ be the maximum of the moduli of the five coordinates $z_i$ and the ten forces $Z_{ij}$. Define $N_w$ in the same way from the $w_i$ and the $W_{ij}$.

For any $a\in\mathbb C^*$, the reciprocal rotation $(z_i,w_i,\delta_{ij})\mapsto(az_i,a^{-1}w_i,\delta_{ij})$ preserves the force and metric equations and multiplies $N_z$ by $|a|$ and $N_w$ by $|a|^{-1}$. It preserves $d_{ij}$, $Q_e$, and $U$. Choosing $a>0$ termwise therefore gives
\[
 N_z=N_w=R:=(N_zN_w)^{1/2}.
\]
We call the resulting sequence \emph{balanced}; subsequent local arguments use this rescaled gauge.

We have $|d_{ij}|\le 4N_zN_w$ and $|Q_e|\le 4^4(N_zN_w)^4$. Hence if a four-product has a pole along the sequence, then $R\to\infty$. Write $R=\eps^{-2}$, so that $\eps\to0$.

After division by $R$, the finite list of coordinates and forces becomes a bounded vector. A common subsequence therefore converges. Finitely many further extractions yield every order comparison and every nonzero root limit used below. All symbols $\asym$, $o(\cdot)$, $\ll$ refer to the extracted subsequence.

\begin{definition}[Circles and strokes]\label{def:strokes}
A \emph{$z$-circle} at $i$ means $|z_i|\asym R$. A \emph{$z$-stroke} on $ij$ means $|Z_{ij}|\asym R$. Absence of a circle or stroke means that the corresponding quantity is $o(R)$. The definitions in the $w$-color are identical. An edge is \emph{double} if it carries both strokes. A stroke is \emph{maximal} if the projected difference in its own color is $\asym R$; for a $z$-stroke this means $|z_i-z_j|\asym R$.
\end{definition}

The metric identity implies
\begin{equation}\label{eq:metric-moduli}
 |Z_{ij}W_{ij}|=|r_{ij}|^{-4},\qquad
 |Z_{ij}|=(|r_{ij}|\,|w_i-w_j|)^{-1},\qquad
 |W_{ij}|=(|r_{ij}|\,|z_i-z_j|)^{-1}.
\end{equation}
Equivalently, $|r_{ij}|^2=|z_i-z_j|\,|w_i-w_j|$ and $|Z_{ij}|=|r_{ij}|^{-3}|z_i-z_j|$.

\begin{lemma}[Edge scales]\label{lem:edgescales}
For every edge $ij$ of a balanced sequence:
\begin{enumerate}
\item $\eps\le|r_{ij}|$ and $|r_{ij}|\lesssim R$.
\item $|z_i-z_j|,\ |w_i-w_j|\gtrsim\eps^2$.
\item On a $z$-stroke,
\[
 |z_i-z_j|\asym R|r_{ij}|^3,\qquad
 |w_i-w_j|\asym (R|r_{ij}|)^{-1},\qquad
 \eps\lesssim|r_{ij}|\lesssim1 .
\]
\item On a double edge, both projected differences and the radius are $\asym\eps$.
\item On a maximal simple $z$-edge, the radius is $\asym1$, the long difference $|z_i-z_j|$ is $\asym R$, and the short difference $|w_i-w_j|$ is $\asym R^{-1}$.
\item On a simple nonmaximal $z$-edge, $\eps\ll|r_{ij}|\ll1$.
\end{enumerate}
The same statements hold with the colors exchanged.
\end{lemma}

\begin{proof}
(1) Balancing gives $|Z_{ij}|,|W_{ij}|\le R=\eps^{-2}$. By \eqref{eq:metric-moduli}, $|r_{ij}|^{-4}\le R^2=\eps^{-4}$, so $|r_{ij}|\ge\eps$. The coordinate bounds give $|z_i-z_j|,|w_i-w_j|\le2R$, so $|r_{ij}|\lesssim R$.

(2) We have $|W_{ij}|^2|w_i-w_j|=|z_i-z_j|^{-3}$, and the left side is $O(R^3)$. Hence $|z_i-z_j|\gtrsim R^{-1}=\eps^2$. The counterpart identity gives the same bound for $|w_i-w_j|$.

(3) Combine $|Z_{ij}|\asym R$ with $|Z_{ij}|=|r_{ij}|^{-3}|z_i-z_j|$ and $|w_i-w_j|=|r_{ij}|^2/|z_i-z_j|$. Then $|z_i-z_j|\lesssim R$ gives $|r_{ij}|\lesssim1$, and the lower bound comes from~(1).

(4) Here $|r_{ij}|^{-4}=|Z_{ij}||W_{ij}|\asym R^2$, so $|r_{ij}|\asym\eps$. By~(3), $|z_i-z_j|\asym R\eps^3=\eps$. Symmetrically, $|w_i-w_j|\asym\eps$.

(5) Combine $|z_i-z_j|\asym R$ with~(3).

(6) The other stroke is absent, so $|W_{ij}|=o(R)$. Hence $|r_{ij}|^{-4}=|Z_{ij}||W_{ij}|=o(R^2)$, which gives $|r_{ij}|\gg\eps$. Nonmaximality means $|z_i-z_j|=o(R)$, and~(3) then gives $|r_{ij}|\ll1$.
\end{proof}

By~(4), a double edge has projected differences $\asym\eps=o(R)$. Hence every maximal stroke is simple.

We also use the elementary triangle rule of~\cite[Section~2, Rule~2e]{ChangThesis}. The three edges of any triangle of edges in the diagram have the same type, and their projected differences are comparable in each color.

\begin{lemma}[Isolated color components]\label{lem:isolated}
Let $C$ be an isolated component of the $z$-strokes. Then $\sum_{i\in C}m_iz_i=o(R)$. If $C$ carries a $z$-circle, then $C$ contains a maximal $z$-difference. The same holds in the $w$-color.
\end{lemma}

\begin{proof}
Sum the $z$-force equations over $C$ with weights $m_i$. The internal forces cancel in pairs. Every external force lacks a stroke and is therefore $o(R)$. This proves the first claim.

For the second claim, suppose every internal difference of $C$ were $o(R)$. Fix $k\in C$. Then $z_i=z_k+o(R)$ for every $i\in C$, so $\bigl(\sum_{i\in C}m_i\bigr)z_k=o(R)$. Positivity of the masses gives $z_k=o(R)$, and hence every coordinate of $C$ would be $o(R)$. This contradicts the circle.
\end{proof}

These statements also account for the entrance estimates in the case table below.

\subsection{Cases and their analytic entrances}

The descriptions below use the numbering of~\cite{AK}. The letters of the two colors may be exchanged. Every permutation acts simultaneously on masses, coordinates, and products.

\begin{center}\small
\begin{tabular}{p{16mm}p{113mm}}\toprule
Case&Support and consequence used in this article\\\midrule
D1, D4&Isolated circled $z$-pair $12$ and uncircled triple $345$. The triple is simple $w$ (D1) or double (D4). The pair is maximal, the triple radii tend to zero, and the crossed $z$-forces are $o(R)$.\\
D2&Circled $z$-pair $12$ and circled simple $w$-triangle $345$. Each internal edge is maximal in its color. Crossed projected differences are $\asym R$ in both colors.\\
D3&Alternating four-cycle with all four vertices circled in both colors, and an uncircled fifth vertex. Each side is maximal in its color. All nonside radii escape.\\
D5&One uncircled double triangle, no other strokes, and no circles. All coordinates are $o(R)$, and the internal differences are $O(\eps)$.\\
D6&Simple wings $125$ in $z$ and $345$ in $w$, with $z$-circles at $1,2$ and $w$-circles at $3,4$. All wing edges are maximal.\\
D7&The same simple wings, with no circles. The wing radii lie strictly between $\eps$ and $1$, and the triangle rule gives the two wing scales.\\
D8&Simple $z$-wing $125$ without circles, and simple $w$-wing $345$ with circles at $3,4$. The $w$-wing is maximal. The $z$-wing has long scale $A$ with $\eps\ll A\ll R$.\\
D9&Double triangle $123$, simple $w$-attachments $14$ and $25$, with $w$-circles at all vertices.\\
D10--D13&Double triangle $125$ and simple $w$-triangle $345$. The precise circle variants are not needed for the upper bounds below.\\
D14, D15&A complete double $K_4$ on $1234$. D14 has no attachment or circles. D15 has one simple $w$-edge $15$, with all five vertices $w$-circled.\\
D16&All ten edges are double.\\\bottomrule
\end{tabular}\end{center}

Where the support alone might hide a step, we give the details.

In D2, by Lemma~\ref{lem:isolated}, the circled isolated pair has a long difference. By the same lemma, the circled isolated triangle has at least one long difference, and the triangle rule makes all three long. All other coordinates in the relevant color are $o(R)$, so the crossed projected differences are $\asym R$ in both colors. It follows that the internal inverse distances have finite nonzero subsequential limits (Lemma~\ref{lem:edgescales}(5)). The crossed inverse distances are $\asym R^{-1}$.

In D3, the isolated color-pair centers and the opposite short differences give the determinant condition $m_1m_3=m_2m_4$, as detailed in the four-cycle section.

In D6 and D8, all coordinates other than those of the circled lower pair are $o(R)$ in that color. Hence the pair is separated at order $R$, and the triangle rule makes the whole lower wing maximal.

In D8, the upper wing is simple and nonmaximal. By the strict endpoint inequality in Lemma~\ref{lem:edgescales}(6), its radius $r$ satisfies $r\gg\eps$, so the long scale $A\asym Rr^3$ satisfies $A\gg\eps$. Since the wing carries no circles, $A\ll R$. The formula $A\asym Rr^3$ and the metric give the short scale
\[
 B\asym R^{-2/3}A^{-1/3}.
\]

In D7, write $a,b$ for the two wing radii. A simple stroke has long difference comparable to $R$ times the cube of its radius, while the product of its projected differences equals the squared radius. Thus the long scales are $Ra^3,Rb^3$ and the short scales are $R^{-1}/a,R^{-1}/b$, respectively. With $R=\eps^{-2}$, these are the scales used in Section~\ref{sec:shorter}.

For D5, Section~\ref{subsec:D5} derives the internal reciprocal-mass relation from the leading equations.

\subsection{The D5 mass relation from the leading equations}\label{subsec:D5}

The collapsing triangle imposes a relation on its three masses. We express it through the symmetric polynomial
\[
 \Phi(a,b,c):=a^2b^2+a^2c^2+b^2c^2-2abc(a+b+c).
\]
\begin{lemma}\label{lem:D5mass}
Let $a,b,c>0$ be the internal masses of a D5 double triangle. Then one of $a^{-1/2},b^{-1/2},c^{-1/2}$ equals the sum of the other two; that is, $\Phi(a,b,c)=0$.
\end{lemma}

\begin{proof}
Divide the internal $z$- and $w$-differences of the triangle by $\eps$, and multiply the internal inverse distances by $\eps$, so that by Lemma~\ref{lem:edgescales}(4) the rescaled quantities have finite nonzero limits after extraction.

There are no circles, and all crossed forces are $o(R)$. Hence the leading internal forces vanish in each coordinate. In other words, the inverse-cube Laplacian of the limiting triangle annihilates both limiting coordinate vectors, $z$ and $w$, after choosing their representatives in the mass-centered subspace
\[
 V=\{(x_1,x_2,x_3)\in\mathbb C^3: ax_1+bx_2+cx_3=0\}.
\]

Suppose the two vectors were linearly independent in the two-dimensional space $V$. Then the Laplacian would vanish on that space. It also vanishes on the constant vector, so it would vanish identically. This contradicts its nonzero off-diagonal entries. Hence the two vectors are proportional. The proportionality constant is nonzero by the metric equations.

Translate and scale the leading $z$-positions to $(0,1,x)$, with $x\neq0,1$. Write the proportional $w$-differences using a square root of the proportionality constant. Solving the three metric equations, the limiting inverse distances equal one common nonzero factor times
\[
 \frac{s_{ij}}{z_j-z_i},\qquad s_{ij}\in\{\pm1\}.
\]

The first two zero-force equations give
\[
 x^2=-\frac{c\,s_{13}}{b\,s_{12}},\qquad
 (x-1)^2=\frac{c\,s_{23}}{a\,s_{12}} .
\]
Both squares are real. Since $(x-1)^2-x^2=1-2x$, the vanishing of the imaginary parts forces $x$ to be real. The squares are nonzero, so they are positive. Therefore
\[
 x=\pm\sqrt{c/b},\qquad x-1=\pm\sqrt{c/a}.
\]

Subtracting these gives a signed linear relation among $a^{-1/2},b^{-1/2},c^{-1/2}$. For three positive numbers, such a relation means that one of them equals the sum of the other two. This is exactly $\Phi(a,b,c)=0$.
\end{proof}

This supplies the mass relation used to define the complete product in Section~\ref{sec:local}.

\section{The local statement and the global reduction}\label{sec:local}
The D5 relation $\Phi=0$ identifies the mass triples that can collapse in the remaining degeneration. To choose a product before selecting any singular sequence, we include every triple allowed by the fixed masses. With $\Phi$ as in Section~\ref{subsec:D5}, define
\[
 \calR(m)=\{e:\Phi(m_k,m_l,m_r)=0,\ \{k,l,r\}=\{1,\ldots,5\}\setminus e\}.
\]
Put $P_m=\prod_{e\in\calR(m)}Q_e$, with empty product one.
\begin{proposition}[Physical-level pole decay]\label{hyp:decay}
For each positive $m$, each real $u>0$ with $Mu^3\ge S^3$, and every sequence $x_k\in X_{m,u}$ for which $|Q_e(x_k)|\to\infty$ for some edge $e$, there is a subsequence on which $P_m(x_k)\to0$.
\end{proposition}
We prove Proposition~\ref{hyp:decay} by the local analysis below and assemble its proof in Section~\ref{sec:obligations}. First we record how it yields the main theorem.
\begin{proposition}[Global reduction]\label{thm:conditional}
If Proposition~\ref{hyp:decay} holds for a fixed positive mass vector $m$ on every physically admissible potential level, then its planar physical central configurations have finitely many proper-similarity classes.
\end{proposition}
\begin{proof}
Each $Q_e$ is a nowhere-zero polynomial on the affine set $X_{m,u}$. The finite-distance reconstruction proves that finite images of all ten $Q_e$ imply finiteness of that set. The two-selection principle, with precisely the fixed index set $\calR(m)$, therefore proves finiteness of each admissible $X_{m,u}$. There are finitely many possible $u$ by the finite-potential-values lemma. Every normalized physical configuration has a representative in the fixed-pair gauge and has admissible $u$. A finite union of these finite fibers contains representatives of all proper-similarity classes. Taking its quotient is finite.
\end{proof}
The local sections are ordered by mechanism. We first establish the D5 decay estimate and the shorter energy and boundedness arguments, then treat the longer compatibility and torque calculations. The table records the conclusion needed in each case; all cases are considered on the fixed admissible level, while the D6 exclusion holds more generally.
\begin{center}\small
\begin{tabular}{lll}\toprule
Diagrams & Mechanism and conclusion & Section\\\midrule
D5 & Collapsing triple: $P_m\to0$ & \ref{sec:D5}\\
D1, D3, D4 & Energy gap: exclusion & \ref{sec:shorter}\\
D7 & Fixed potential: bounded four-products & \ref{sec:shorter}\\
D8 & Crossed compatibility and energy: exclusion & \ref{sec:D8}\\
D2 & Triple response and torque: exclusion & \ref{sec:D2}\\
D6 & Fourth-order torque: exclusion & \ref{sec:D6}\\
D9 & Attached-triangle energy: exclusion & \ref{sec:D9}\\
D10--D16 & Direct four-product bounds & \ref{sec:back}\\\bottomrule
\end{tabular}
\end{center}


\section{The complete exceptional product}
A D5 limit makes the four-product complementary to its collapsing triple decay rapidly, but that triple may differ between the two selections. The product $P_m$ therefore includes every complementary triple allowed by the fixed masses. The bound below limits this product to six factors; Section~\ref{sec:obligations} uses the resulting decay after the local estimates have been established.

\begin{lemma}\label{lem:six}
For every positive five-tuple $m$, $\norm{\calR(m)}\le6$.
\end{lemma}
\begin{proof}
Put $a_i=m_i^{-1/2}>0$. For three masses $x,y,z$ and their reciprocal square roots $a,b,c$,
\[
 \frac{\Phi(x,y,z)}{(xyz)^2}
 =(c-a-b)(c+a+b)(c-a+b)(c+a-b).
\]
After taking $c$ to be the largest, the last three factors are positive. Thus $\Phi(x,y,z)=0$ precisely when one reciprocal root is the sum of the other two.

Order the five labelled values as $a\le b\le c\le d\le e$. Among the first four labels the possible additive triples correspond to
\[
 a+b=c,\quad a+b=d,\quad a+c=d,\quad b+c=d.
\]
All four equations cannot hold, so there are at most three such triples. Triples involving the last label correspond to pairs among the first four whose sum is $e$. The graph of these pairs is a union of complementary complete bipartite blocks and a clique on the values $e/2$.

On four vertices that graph either has at most three edges, has four edges as $K_{2,2}$, or has six edges as $K_4$; five edges are impossible. At most three edges give a total of at most six. Four edges force first-four values $(x,x,y,y)$, $x<y$, with $e=x+y$; these support at most two internal additive triples, namely $x+x=y$. Six edges force all first-four values to equal $e/2$, with no internal additive triple. Every case gives the claimed bound. Equal numerical values retain distinct labels throughout.
\end{proof}


\section{D5: a complete exterior-scale argument}\label{sec:D5}
The following estimate holds for arbitrary sequences satisfying the stated scale bounds.
\begin{lemma}[Three-point collapsing cluster]\label{lem:d5}
Consider solutions of \eqref{eq:complexforce}--\eqref{eq:metric} at a fixed physically admissible potential $u$. Let $T$ be a triple of total mass $K$, and let its complementary bodies have masses $p,q$, with $P=p+q$ and $M=K+P$. Suppose there is a positive scale $\eps\to0$ such that every coordinate is $o(\eps^{-2})$ and every internal $z$- and $w$-difference in $T$ is $O(\eps)$. Then every noninternal squared distance is $o(\eps^{-1})$.
\end{lemma}
\begin{proof}
Let $C_T^z,C_T^w$ be the actual mass-weighted triple center. Write $z_i=C_T^z+e_i$, $w_i=C_T^w+f_i$ for $i\in T$. Then $e_i,f_i=O(\eps)$, their mass-weighted sums vanish, and $J=\sum_Tm_ie_if_i=O(\eps^2)$. Write $r_{ij}=\delta_{ij}^{-1}$ on the selected metric sheet, so $r_{ij}^2=d_{ij}$.

First suppose all six cross radii tend to infinity in modulus. Let $\eta$ be the maximum modulus of their inverse cubes, so $\eta\to0$. In either color let $C_P$ be the exterior-pair center, $X=C_P-C_T$, and $D$ the difference of the two exterior coordinates. Centering gives $C_P=KX/M$, $C_T=-PX/M$. The cross differences are exactly
\[
 X+(q/P)D-\mathrm{internal}_i,\qquad
 X-(p/P)D-\mathrm{internal}_i.
\]
The mass-weighted exterior force sum cancels the mutual pair force. Absorbing its $O(\eta)|X|$ term, and then taking the exterior force difference, gives
\begin{equation}\label{eq:d5center}
 X=O(\eta)(|D|+\eps),\qquad
 (1-Pr_{ab}^{-3})D=O(\eta)(|D|+\eps).
\end{equation}
At least one projected cross difference is unbounded, because its squared radius is unbounded. After a subsequence and color interchange, $|D_z|\to\infty$. Division of the second equation by $D_z$ proves $r_{ab}^3\to P$. Hence $d_{ab}$ stays bounded and bounded away from zero, and $D_w=O(|D_z|^{-1})$.

All triple-to-exterior $z$-differences are comparable to $D_z$, with nonzero limiting coefficients $q/P$ and $-p/P$. The exact metric identity gives
\[
 \left|\frac{w_a-w_i}{r_{ai}^3}\right|
 =\frac1{|r_{ai}|\,|z_a-z_i|}=o(|D_z|^{-1}).
\]
The exterior weighted $w$-force sum and the total centroid now imply $X_w=o(|D_z|^{-1})$. Equation~\eqref{eq:d5center} gives $X_z=o(|D_z|)$, so $X_zX_w\to0$. The exact three-block decomposition is
\begin{equation}\label{eq:d5inertia}
 u=I=J+\frac{pq}{P}d_{ab}+\frac{KP}{M}X_zX_w.
\end{equation}
Cubing the limit yields $u^3=(pq)^3/P$. But $S>pq+PK$ and $P^2>pq$ give
\[
 \frac S{pq}>1+\frac{PK}{pq}>\frac MP>1,
 \qquad \frac{S^3}{M}>\frac{(pq)^3}{P},
\]
contradicting the physical floor. Thus the all-cross-escape alternative is impossible.

Next pass to a subsequence with one bounded cross squared distance, say $d_{ai_0}$. Relative to the exact triple center put
\[
 x_a=z_a-C_T^z,\quad y_a=w_a-C_T^w,\quad
 x_b=z_b-C_T^z,\quad y_b=w_b-C_T^w.
\]
These coordinates are $o(\eps^{-2})$, so, uniformly over $i\in T$,
\begin{equation}\label{eq:d5metric}
 d_{ci}=(x_c-e_i)(y_c-f_i)=x_cy_c+o(\eps^{-1}).
\end{equation}
Consequently $x_ay_a=o(\eps^{-1})$. Centering also gives the exact identity
\[
 M(u-J)=p(K+q)x_ay_a+q(K+p)x_by_b-pq(x_ay_b+x_by_a).
\]
If $x_by_b$ were not $o(\eps^{-1})$, retain a subsequence with $H=x_by_b$ satisfying $|H|\ge c\eps^{-1}$ for some $c>0$. Since both coordinates are $o(\eps^{-2})$, each of $|x_b|/\eps$ and $|y_b|/\eps$ tends to infinity. Thus $d_{bi}/H\to1$ for all $i\in T$.

Set $t=x_a/x_b$ and $v=y_a/y_b$. The previous identity, divided by $H$, gives
\[
 tv\to0,\qquad t+v\to(K+p)/p.
\]
The roots of a quadratic depend continuously as an unordered pair on its coefficients. After a subsequence and possible color exchange, $t\to0$ and $v\to(K+p)/p$. Therefore
\[
 d_{ab}/H=(1-t)(1-v)\to-K/p\ne0.
\]
Every radius incident to $b$ now tends to infinity. On the other hand, centering gives
\[
 z_b/x_b=\frac{K+p-pt}{M}\longrightarrow\frac{K+p}{M}\ne0.
\]
The actual force equation gives the contradictory limit
\[
 z_b/x_b=\sum_{i\in T}m_ir_{bi}^{-3}(1-e_i/x_b)
                 +p r_{ab}^{-3}(1-t)\longrightarrow0.
\]
Thus $x_by_b=o(\eps^{-1})$. Equation~\eqref{eq:d5metric} controls all six cross distances. Finally
\[
 MI=\sum_{i<j\in T}m_im_jd_{ij}
       +p\sum_{i\in T}m_id_{ai}+q\sum_{i\in T}m_id_{bi}+pq d_{ab}
\]
controls the seventh noninternal distance, $d_{ab}=o(\eps^{-1})$.

To remove the subsequence alternatives, suppose one of these conclusions fails, and retain a fixed positive lower bound for its scaled modulus. Successively extract for each of the six cross radii a subsequence on which it is bounded or tends to infinity. All six escaping is impossible by the first argument; a bounded one contradicts the retained failure by the second argument. The finite extraction proves the assertion for the original sequence.
\end{proof}

\begin{corollary}[Product decay from a D5 chart]\label{cor:d5}
In addition to Lemma~\ref{lem:d5}, suppose $\Phi(m_i,m_j,m_k)=0$ for the internal triple $T$. Then $P_m\to0$.
\end{corollary}
\begin{proof}
Let $e_0$ be the edge complementary to $T$. Its four-product contains three internal squared distances of order $O(\eps^2)$ and one noninternal distance, so $Q_{e_0}=o(\eps^5)$. Every other four-product contains exactly one internal and three noninternal squared distances, so $Q_e=o(\eps^{-1})$. To check the incidence statement, a different triple meets $T$ in either two vertices, giving factors $d_{ij}d_{ia}d_{ja}d_{kb}$, or one vertex, giving $d_{jk}d_{ia}d_{ib}d_{ab}$.

The complete mass-only list has $k\le6$ elements, and contains $e_0$. Hence
\[
 P_m=o(\eps^5)O(\eps^{-(k-1)})=o(\eps^{6-k})\to0.
\]
For $k=1$ the other-factor product is one. For $k=6$ strict little-$o$, rather than boundedness, is essential.
\end{proof}
The classified entrance estimates and the internal reciprocal-mass relation were derived in Section~\ref{sec:entrance}. Thus this estimate applies to every D5 subsequence throughout the permitted exterior-scale range.

\section{Three shorter local mechanisms}\label{sec:shorter}
\subsection{D1 and D4: the isolated pair}
Suppose the balanced maximum is $R=\eps^{-2}$, the pair $12$ has $|z_1|,|z_2|,|z_1-z_2|\asym R$, the triple $T=\{3,4,5\}$ has $z_i=o(R)$, its internal squared distances tend to zero, and all pair-to-triple $z$-forces are $o(R)$. Put $p=m_1$, $q=m_2$, $P=p+q$, and $K=\sum_Tm_i$.

Cross $z$-differences are $\asym R$, so their inverse cubes tend to zero. Their $w$-forces are $o(R^{-1})$ by the metric identity used in Lemma~\ref{lem:d5}. The exterior weighted force sum and centering give $w_P,w_T=o(R^{-1})$ and $z_P,z_T=o(R)$. Subtracting the pair $z$-equations gives $\delta_{12}^3\to1/P$. The exact decomposition
\[
 u=\frac{pq}{P}d_{12}+\frac1K\sum_{i<j\in T}m_im_jd_{ij}
       +\frac{PK}{M}(z_P-z_T)(w_P-w_T)
\]
therefore gives $u^3=(pq)^3/P$, contradicting the strict physical-floor comparison in the preceding proof. Thus D1 and D4 are excluded.

\subsection{D3: a four-cycle energy gap}
Choose the colors so that the $z$-strokes are $12,34$ and the $w$-strokes are $23,41$. Vertices $1,2,3,4$ are circled in both colors. Write $\zeta_i=\lim z_i/R$ after extraction. The short $z$-differences on the $w$-strokes give
\[
 \zeta_1=\zeta_4=A\ne0,\qquad \zeta_2=\zeta_3=B\ne0.
\]
The two isolated $z$-pairs satisfy Lemma~\ref{lem:isolated}, hence
\[
 m_1A+m_2B=0,\qquad m_4A+m_3B=0.
\]
Multiply the first equation by $m_3$ and the second by $m_2$, then subtract. Since $A\ne0$, this proves
\[
 m_1m_3=m_2m_4=:\Pi>0.
\]
In particular $A\ne B$, by positivity. The same argument in the other color shows that both diagonals have projected differences of order $R$ in both colors. The fifth vertex is uncircled, so its differences from the four circled vertices also have order $R$ in both colors. All nonside inverse distances therefore tend to zero.

Each side is a maximal isolated edge in its own color. Subtracting its endpoint force equations, whose other terms are $o(R)$, and dividing by the corresponding difference gives
\[
 \delta_{ij}^3\longrightarrow\frac1{m_i+m_j}
 \qquad(ij=12,23,34,41).
\]
Put $K=m_1+\cdots+m_4$, $J=\sum_{1\le i<j\le4}m_im_j$, $c=m_5$, and
\[
 T=\sum_{ij\text{ on the cycle}}\frac{m_im_j}{(m_i+m_j)^{1/3}}.
\]
Pass to a common subsequence on which the four side inverses converge, and write their limits as $\rho_{ij}$. Since every nonside inverse tends to zero, the potential decomposes as
\[
 u=\sum_{ij\text{ on the cycle}}m_im_j\rho_{ij},\qquad
 \rho_{ij}^3=(m_i+m_j)^{-1}.
\]
Each $\rho_{ij}$ has modulus $(m_i+m_j)^{-1/3}$. The triangle inequality therefore gives $|u|\le T$, independently of the four choices of cube root.

For an edge with product $w=m_im_j$ and sum $q=m_i+m_j$, the complementary masses satisfy $w(m_k+m_l)=\Pi q$. Since $(1+x)^{1/3}<1+x/3$ for $x>0$,
\[
 K^{1/3}w/q^{1/3}<w+\Pi/3.
\]
Summing the four inequalities yields $K^{1/3}T<J-2\Pi/3<J$. Also $J<K^2/2$, and direct expansion gives
\[
 K(J+cK)^3-(K+c)J^3
 =c\{J^2(3K^2-J)+3cJK^3+c^2K^4\}>0.
\]
Thus $|u|^3\le T^3<J^3/K<S^3/M$, impossible at a physical level.

\subsection{D7: boundedness suffices}
Consider two simple wings $125$ and $345$, with no circles, in opposite colors. The entrance estimates give the scales
\[
 \eps\ll a,b\ll1,\quad Z=\eps^{-2}a^3,\quad W=\eps^{-2}b^3,
 \quad u_s=\eps^2/a,\quad v_s=\eps^2/b.
\]
All upper wing radii are comparable to $a$, its long $z$-differences to $Z$, and its short $w$-differences to $u_s$; the lower wing has radii $b$, long differences $W$, and short differences $v_s$. Hence the four crossed squared distances are comparable to $ZW$. Their force moduli are
\[
 O(\eps^4a^{-3/2}b^{-9/2}),\qquad
 O(\eps^4a^{-9/2}b^{-3/2}).
\]
Let $A_z$ and $B_z$ be the forces on body 5 from its upper and lower wings. The body-5 equation, the weighted upper force sum, and centering give, with $C_z$ a weighted crossed-force sum,
\[
 z_5=A_z+B_z,\quad m_1z_1+m_2z_2=-m_5A_z+C_z,
 \quad (m_3+m_4)z_5=-m_5B_z-C_z+O(v_s).
\]
The lower short-force scale bounds $B_z=O(\eps^2/b^4)$; the cross term is smaller. Thus $z_5=O(\eps^2/b^4)$. Reversing colors gives $w_5=O(\eps^2/a^4)$. The exact shifted inertia identity implies
\[
 |u|\le C\{a^2+b^2+(\eps/(ab))^4\}.
\]
The two wing four-products have orders $a^6b^2$ and $a^2b^6$. Each of the other eight contains one upper, one lower, and two crossed squared distances, so its modulus is comparable to $(ab/\eps)^8$. A pole therefore forces $ab/\eps\to\infty$, and the displayed inertia bound forces $u=0$. Thus a nonzero fixed potential rules out a four-product pole, which is the conclusion required for D7 in the global reduction.

\section{D8: crossed compatibility before the energy comparison}\label{sec:D8}

\subsection{Chart hypotheses and the conclusion}
In the D8 roles, the masses of bodies $1,\dots,5$ are $(p,q,a,b,c)$, all
positive. We work on the fixed level $U=I=u>0$ satisfying $Mu^3\ge S^3$. The upper wing is $125$, the lower wing is $345$, and body $5$
is common to both wings. The parameter $R\to\infty$ is the balanced
maximum, and $A$ is the upper long $z$-scale. We write
$z_{ij}=z_i-z_j$ and use the same convention for $w_{ij}$. The starting
estimates are
\begin{gather}
 R^{-1/2}\ll A\ll R,\qquad B\asym R^{-2/3}A^{-1/3},\label{eq:d8scales}\\
 |z_{12}|,|z_{15}|,|z_{25}|\asym A,\quad
 |w_{12}|,|w_{15}|,|w_{25}|\asym B.\nonumber
\end{gather}
The three lower $z$-differences are $\asym R^{-1}$, and the three lower
$w$-differences are $\asym R$. Their inverse distances have nonzero
finite limits. The circle data in Section~\ref{sec:entrance} give
$w_1,w_2,w_5=o(R)$ and $|w_3|,|w_4|\asym R$. Exact centering then gives
$aw_3+bw_4=o(R)$. Thus these conditions and \eqref{eq:d8scales} all follow from the classified support.

Under these hypotheses, we show that the full equations force the mass
pattern
\begin{equation}\label{eq:d8pattern}
 p=q=\mu,\qquad c=\mu/4,\qquad a=b.
\end{equation}
In the last subsection we exclude this pattern at the physical level.
The order of the argument matters: crossed compatibility must be
established before the energy comparison, because the analogous energy
comparison is false for arbitrary unequal lower masses.

The crossed forces between the two wings have the scales
\[
 X=A^{-1/2}R^{-3/2}=o(R^{-1}),\qquad
 C=A^{-3/2}R^{-1/2}.
\]
Here $X=o(R^{-1})$ because $XR=(AR)^{-1/2}\to0$. The lower $z$-equations
imply $z_3,z_4=O(R^{-1})$, and a lower difference then gives
$z_5=O(R^{-1})$. By centering, $pz_1+qz_2=O(R^{-1})$.

\subsection{The upper sheets and an exact local force law}
Put $h=p+q$ and
\[
 s=(z_1-z_2)/h,\quad
 x=\frac{(pz_1+qz_2)/h-z_5}{s}.
\]
Then $|s|\asym A$. Since $pz_1+qz_2$ and $z_5$ are $O(R^{-1})$, we get
$x=O((AR)^{-1})$. Writing
$z_1=(pz_1+qz_2)/h+q(z_1-z_2)/h$, and $z_2$ similarly, gives exactly
\[
 z_1=z_5+s(q+x),\qquad z_2=z_5+s(x-p),
\]
so that $z_{15}=s(q+x)$ and $z_{25}=s(x-p)$.

The upper internal $z$-forces have scale $R$, whereas the full left
sides are $O(A)=o(R)$. The crossed $z$-forces are $O(X)=o(R)$. Pass to a
subsequence along which the ratios
$v_{15}=\lim\delta_{15}/\delta_{12}$ and
$v_{25}=\lim\delta_{25}/\delta_{12}$ exist and are nonzero. In the
$z$-equation of body~$1$, the forces exerted by bodies $2$ and $5$ must
therefore cancel to leading order. Dividing by
$\delta_{12}^3z_{12}$ and using $z_{15}/z_{12}=(q+x)/h\to q/h$ gives
$q+cv_{15}^3q/h=0$. Body~$2$ gives the same relation for $v_{25}$,
because $z_{25}/z_{21}\to p/h$. Hence
\[
 v_{15}^3=v_{25}^3=-h/c.
\]

Set $\kappa=v_{25}/v_{15}$. Then $\kappa^3=1$. By the metric identity
$\delta_{ij}^3w_{ij}=\delta_{ij}/z_{ij}$, we have
$w_{ij}=(\delta_{ij}^2z_{ij})^{-1}$. Substituting this into the exact
cycle $w_{15}-w_{25}=w_{12}$ and multiplying by $\delta_{12}^2s$ gives,
in the limit,
\[
 \frac1{qv_{15}^2}+\frac1{pv_{25}^2}=\frac1h .
\]
Since $\kappa^{-2}=\kappa$, this is
\[
 v_{15}^2=\frac{h(p+q\kappa)}{pq}.
\]
Comparing its cube with $v_{15}^6=h^2/c^2$ gives
\[
 c^2h(p+q\kappa)^3=p^3q^3 .
\]
The right side is positive. Suppose $\kappa=\omega$ is a primitive cube
root of unity. Then
$\operatorname{Im}(p+q\omega)^3=\pm3\sqrt3\,pq(p-q)/2$, with the sign
fixed by the choice of $\omega$. This is nonzero if $p\ne q$. If $p=q$,
then $(p+q\omega)^3=p^3(1+\omega)^3=-p^3<0$. Neither case is compatible
with the positive right side, so
\[
 \kappa=1,\quad c=(pq)^{3/2}/h^2,\quad
 v_{15}=v_{25}=-h/\sqrt{pq}.
\]
The square $v_{15}^2=h^2/(pq)>0$ gives $v_{15}=\pm h/\sqrt{pq}$, and the cube $v_{15}^3=-h/c<0$ selects the negative sign.

Next set $r=(w_1-w_2)/h$,
\[
 y=\frac{(qw_1+pw_2)/h-w_5}{r},\qquad D=h\delta_{12}.
\]
The same decomposition as for $z$ gives exactly
\[
 w_1=w_5+r(p+y),\qquad w_2=w_5+r(y-q).
\]
Note that the weights on $w_1,w_2$ in $y$ are swapped relative to those
in $x$. The metric relation for $12$ reads $D^2sr=1$. With
\eqref{eq:d8scales}, it gives $|r|\asym B$ and
$|D^3s|\asym(AB)^{-3/2}A\asym R$. The metric relation for $15$ gives
$\delta_{15}^{-2}=z_{15}w_{15}=(q+x)(p+y)/D^2$. So
\[
 \frac{\delta_{15}^2}{\delta_{12}^2}=\frac{h^2}{(q+x)(p+y)}\to v_{15}^2=\frac{h^2}{pq}.
\]
Since $x\to0$, it follows that $y\to0$.

Take the local analytic roots that are positive at the positive real
reference arguments. The sheets already selected for
$v_{15},v_{25}$ give
\[
 \delta_{15}=-D(q+x)^{-1/2}(p+y)^{-1/2},\quad
 \delta_{25}=-D(p-x)^{-1/2}(q-y)^{-1/2}.
\]
These formulas hold eventually along the sequence. Let $K=(pq)^{3/2}$, so that
$ch^2=K$. Then the upper internal $z$-forces on bodies $1,2$ are
$D^3s/h^2$ times $Z_1,Z_2$, and the upper internal $w$-forces are
$D^3r/h^2$ times $W_1,W_2$, where
\begin{align*}
 Z_1&=q-K(q+x)^{-1/2}(p+y)^{-3/2},&
 Z_2&=-p+K(p-x)^{-1/2}(q-y)^{-3/2},\\
 W_1&=q-K(q+x)^{-3/2}(p+y)^{-1/2},&
 W_2&=-p+K(p-x)^{-3/2}(q-y)^{-1/2}.
\end{align*}
In particular $Z_1(0)=Z_2(0)=0$, but $W_1(0)=W_2(0)=q-p$. Setting
either of the latter equal to zero at this stage would impose an
unjustified mass equality.

We estimate the crossed $w$-force difference separately for $p\ne q$ and $p=q$. Both calculations give $o(C)$; the crossed-sheet equations will then force $p=q$ and $a=b$.

\subsection{Unequal upper masses}
Let $\sigma=|x|+|y|$. Differentiating at the origin gives
\[
 D(Z_1,Z_2)(0)=\begin{pmatrix}1/2&3q/(2p)\\1/2&3p/(2q)\end{pmatrix},
 \qquad\det=\frac{3(p^2-q^2)}{4pq}.
\]
Put $T_z=pZ_1+qZ_2$ and $D_z=Z_1-Z_2$. Taylor expansion and the original
force sums give
\begin{align*}
 T_z&=\tfrac h2(x+3y)+O(\sigma^2)=O(R^{-2}),\\
 D_z&=\tfrac32(q/p-p/q)y+O(\sigma^2)=\nu+o(A/R),\quad
 \nu=h^3/D^3,\quad |\nu|\asym A/R.
\end{align*}
For the force estimates, let $F_i=O(X)$ be the crossed $z$-force on body $i$ and put $K_z=D^3s/h^2$, with $|K_z|\asym R$. The exact equations $z_i=K_zZ_i+F_i$ give
\[
 K_zT_z=pz_1+qz_2-pF_1-qF_2=O(R^{-1})+O(X),
 \qquad K_zD_z=hs-(F_1-F_2).
\]
Thus $T_z=O(R^{-2})$ and $D_z=h^3/D^3+O(X/R)$. The last error is $o(A/R)$ because $X/A=(AR)^{-3/2}\to0$. Each individual $Z_i$ is $O(A/R)$ as well.

Assume $p\ne q$. Then the derivative is invertible. Since $\sigma\to0$,
the quadratic remainder can be absorbed, which gives
$\sigma=O(A/R)$. In particular $O(\sigma^2)=o(A/R)$. Because
$R^{-2}=o(A/R)$, substitution yields
\[
 y=\frac{2\nu}{3(q/p-p/q)}+o(A/R),\qquad
 x=-\frac{2\nu}{q/p-p/q}+o(A/R).
\]
Hence $|x|\asym A/R$. Comparing this with $x=O((AR)^{-1})$ gives
$A^2=O(1)$, that is, $A=O(1)$.

Now consider the $w$-difference. Since $W_1-W_2=O(\sigma)$, the
corresponding dimensional internal force is
$O((RB/A)(A/R))=O(B)$; here $|D^3r/h^2|\asym RB/A$. The full
$w$-difference is also $O(B)$. Therefore the crossed $w$-force
difference is $O(B)$. Moreover,
\[
 B/C\asym(A^7/R)^{1/6}\to0,
\]
since $A=O(1)$. So the crossed $w$-force difference is $o(C)$.

\subsection{Equal upper masses}
Assume $p=q=\mu$. The sheet calculation above then gives
$c=\mu/4$ and $K=\mu^3$. In this case
$Z_2(x,y)=-Z_1(-x,-y)$ and $W_2(x,y)=-W_1(-x,-y)$. Consequently the
weighted sum $T_z$ is odd in $(x,y)$, and the differences $D_z$ and
$W_1-W_2$ are even. Their expansions are
\begin{align*}
 T_z&=\mu(x+3y)+O(\sigma^3),\\
 D_z&=-\frac{3}{4\mu}(x^2+2xy+5y^2)+O(\sigma^4),\\
 W_1-W_2&=-\frac{3}{4\mu}(5x^2+2xy+y^2)+O(\sigma^4).
\end{align*}
Since $\partial_yT_z(0)=3\mu\ne0$, Taylor expansion and absorption
give $|y|=O(|x|+|T_z|)$. As before, $T_z=O(R^{-2})$ and
$x=O((AR)^{-1})$, and $R^{-2}=o((AR)^{-1})$. Hence
$\sigma=O((AR)^{-1})$.

The internal $z$-difference is therefore
$O(R\sigma^2)=O((A^2R)^{-1})$. Its full left side has size $\asym A$, and
the crossed remainder is $O(X)=o(A)$. Therefore
\[
 A^3R=O(1).
\]

The internal $w$-difference is $O((RB/A)\sigma^2)=O(B/(A^3R))$. To compare this term with the crossed-force scale $C$, we use
\[
 \frac{B}{A^3RC}\asym(R^7A^{11})^{-1/6}\to0.
\]
Indeed, if we write $A=R^{-1/2}L$ with $L\to\infty$, this quantity is
$R^{-1/4}L^{-11/6}$. Also $B/C\asym(A^7/R)^{1/6}\to0$, because
$A^3R=O(1)$. The full $w$-difference is $O(B)$. So on this branch too
the crossed $w$-force difference is $o(C)$.

\subsection{All crossed sheets force both equal pairs}
Pass to a further subsequence along which $s/A\to\alpha\ne0$,
$w_3/R\to bH$ and $w_4/R\to-aH$ with $H\ne0$. This form of the limits
expresses the centering $aw_3+bw_4=o(R)$. Along the same subsequence,
let $\delta_{ij}(AR)^{1/2}\to\chi_{ij}$ on the four crossed edges
$13,23,14,24$.

To leading order, $z_{13},z_{14}\sim q\alpha A$ and
$z_{23},z_{24}\sim-p\alpha A$, while $w_{13},w_{23}\sim-bHR$ and
$w_{14},w_{24}\sim aHR$. The metric relations therefore give
\[
 \chi_{13}^2=-\frac1{q\alpha bH},\quad
 \chi_{23}^2=\frac1{p\alpha bH},\quad
 \chi_{14}^2=\frac1{q\alpha aH},\quad
 \chi_{24}^2=-\frac1{p\alpha aH}.
\]
Let $Q=\chi_{13}\ne0$. Keeping every sign, we write
\[
 \chi_{23}=\sigma_0\ii\sqrt{q/p}\,Q,\quad
 \chi_{14}=\tau_0\ii\sqrt{b/a}\,Q,\quad
 \chi_{24}=\upsilon_0\sqrt{qb/(pa)}\,Q,
 \quad\sigma_0,\tau_0,\upsilon_0\in\{\pm1\}.
\]

The metric identity $\delta_{ij}^3w_{ij}=\delta_{ij}/z_{ij}$ turns each
crossed $w$-force $m_j\delta_{ij}^3w_{ij}$ into
$m_j\delta_{ij}/z_{ij}$. Inserting the limits above, the crossed
$w$-force difference between bodies $1$ and $2$, divided by $C$,
converges to
\[
 \frac{aQ}{q\alpha}\{1+\sigma_0\ii\gamma+\rho(\tau_0\ii+\upsilon_0\gamma)\},
 \qquad\gamma=(q/p)^{3/2}>0,\quad\rho=(b/a)^{3/2}>0.
\]
Both previous branches showed that this limit vanishes. Since
$aQ/(q\alpha)\ne0$, the bracket vanishes. Because $\gamma$ and $\rho$
are real, its real and imaginary parts give
\[
 1+\rho\upsilon_0\gamma=0,\qquad \sigma_0\gamma+\rho\tau_0=0.
\]
Positivity of $\rho\gamma$ forces $\upsilon_0=-1$ and $\rho\gamma=1$. The
second equation forces $\tau_0=-\sigma_0$ and $\rho=\gamma$. Hence
$\rho=\gamma=1$, that is, $p=q$ and $a=b$. With $c=\mu/4$ from the
equal-mass sheet calculation, this proves \eqref{eq:d8pattern}. All
sixteen crossed sign choices were retained in the argument. In
particular, the branch $p\ne q$ is impossible.

\subsection{The surviving pattern lies below the physical floor}
The masses are now $(\mu,\mu,a,a,\mu/4)$. Consider the exact
shifted identity
\[
 I=-Mz_5w_5+\sum_{i\ne5}m_i(z_i-z_5)(w_i-w_5).
\]
The shared term vanishes in the limit, since $z_5=O(R^{-1})$ and
$w_5=o(R)$. The upper products have size $AB\asym(A/R)^{2/3}\to0$. Let
$e,f,g$ be the nonzero limiting lower inverses on $34,35,45$. By the
metric relation, the lower products are
$(z_i-z_5)(w_i-w_5)=\delta_{i5}^{-2}$ for $i=3,4$. Hence
$I\to a(f^{-2}+g^{-2})$.

We next derive the lower long relations. Take the mass-weighted sum of the three upper
$w$-equations. The internal upper forces cancel, the crossed forces are
$o(R)$, and the upper left sides are $o(R)$. The remaining forces of
bodies $3,4$ on body $5$ are of order $R$. Since $a=b$ and
$w_4/w_3\to-1$, these give $f^3=g^3$. The first lower relation below
follows by subtracting the equations of bodies $3$ and $4$ after their
weighted leading center relation. Finally, write $z_{ij}=1/(\delta_{ij}^2w_{ij})$
in the exact cycle $z_{34}=z_{35}-z_{45}$ and multiply by $w_3$. Since
$w_3/w_{34}\to1/2$, $w_3/w_{35}\to1$ and $w_3/w_{45}\to-1$, this yields
the squared-distance relation. Together these give
\[
 2ae^3+(\mu/4)f^3=1,\quad f^3=g^3,\quad
 \frac1{2e^2}=\frac1{f^2}+\frac1{g^2}.
\]
Since $I=u$ along the sequence, this gives $u=a/(2e^2)$.

Set $\vartheta=g/f\in\mu_3$ and let
$\eta=f^3/e^3$. Since $\vartheta^{-2}=\vartheta$, the third relation gives
$f^2/e^2=2(1+\vartheta)$, and the first relation can be solved for $e^3$:
\[
 \eta^2=[2(1+\vartheta)]^3,\quad
 e^3=(2a+(\mu/4)\eta)^{-1},\quad
 u=\frac a{2e^2},\quad
 u^3=\frac{a^3}{8}(2a+(\mu/4)\eta)^2.
\]
The first lower relation ensures $2a+(\mu/4)\eta\ne0$.

There are six pairs $(\vartheta,\eta)$. For $\vartheta=1$ we get $\eta=\pm8$.
For $\vartheta$ a primitive cube root of unity,
$[2(1+\vartheta)]^3=-8$, so $\eta=\pm2\sqrt2\ii$. In the latter case
$u^3$ has imaginary part $\pm(\sqrt2/4)a^4\mu\ne0$, so $u^3$ is not
real. For $\eta=\pm8$ we get $u^3=a^3(a\pm\mu)^2/2$. Therefore
every positive-real possibility satisfies
\[
 u^3\le E_+:=a^3(a+\mu)^2/2.
\]
Here
\[
 M=2a+9\mu/4,\qquad S=a^2+(9/2)\mu a+(3/2)\mu^2,
\]
and exact expansion gives
\[
 S^3-ME_+=\frac18\bigl(83\mu a^5+496\mu^2a^4+1044\mu^3a^3
 +783\mu^4a^2+243\mu^5a+27\mu^6\bigr)>0.
\]
This contradicts the physical floor $Mu^3\ge S^3$.

\section{D2: the exact response problem}\label{sec:D2}

The D2 limit consists of a distant pair and triple. The energy inequality restricts the limiting triple to an Euler configuration. We exclude it by studying its response to the pair: the shape equations determine a first-order displacement, and the remaining torque equation imposes a compatibility condition on that displacement.

We work throughout on $U=I=u>0$ with $Mu^3\ge S^3$. The argument has three stages. First, an exact chart extracts the limiting pair and triple and retains the chosen metric roots. Second, after removing the rotational freedom, the implicit-function theorem determines the response whenever the relevant Jacobian is invertible. Differentiating the torque condition then leaves only three alternatives: a zero transverse eigenvalue, the resonant eigenvalue $-1/2$, or zero transverse forcing. Third, algebraic classification and the original torque equation exclude those alternatives. The longer polynomial identities are collected in Appendices~\ref{app:resonance} and~\ref{sec:hcert}.

\subsection{A pair--triple chart}

The pair has masses $p,q$ and is indexed by $i\in\{1,2\}$, with $p_1=p$ and $p_2=q$. The triple has masses $n_1,n_2,n_3$. Put
\[
 A=p+q,\qquad B=n_1+n_2+n_3,\qquad M=A+B .
\]
Use superscripts $P$ and $T$ for pair and triple coordinates, with local indices $i=1,2$ and $k=1,2,3$, respectively. Put $a=(-q,p)$ and write the exact coordinates
\begin{align*}
 z_i^P&=Z_P+h^{-1}a_i,& w_i^P&=W_P+h b_i\quad(i=1,2),\\
 z_k^T&=Z_T+h c_k,& w_k^T&=W_T+h^{-1}d_k\quad(k\text{ in the triple}),
\end{align*}
where $b=\beta a$, $\sum n_kc_k=\sum n_kd_k=0$, $d_3=1$, and
\[
 (Z_T-Z_P,W_T-W_P)=h^2(\eta_z,\eta_w),\qquad h\to0.
\]
Here $Z_P,W_P$ and $Z_T,W_T$ are the weighted centers of the pair and of the triple. Note that $\sum_ip_ia_i=-pq+qp=0$, so $a$ and $b$ are centered automatically.

\paragraph{Extracting the chart.}
We first show that this chart can be extracted from an actual D2 sequence. In the balanced scale $R=\eps^{-2}$, the pair has $z$-difference $\asym R$ and $w$-difference $\asym R^{-1}$. The triple has the opposite scales on every internal edge. Every cross difference is $\asym R$ in both projections. Hence cross inverses are $\asym R^{-1}$, and cross forces are $O(R^{-2})$. In the mass-weighted force sum over either cluster the internal forces cancel. Therefore both coordinates of both exact cluster centers are $O(R^{-2})$.

Let $\Delta z=z_2^P-z_1^P$ be the pair $z$-difference before the new gauge. Let $w_*$ be the $w$-coordinate of the third triple body minus the weighted triple center. Both have modulus $\asym R$, and both are nonzero. Choose
\[
 h^2=\frac{A}{\Delta z\,w_*},\qquad \alpha=\frac{A}{h\Delta z},
\]
and replace $z,w$ by $\alpha z,\alpha^{-1}w$. Then $|h|\asym R^{-1}$, and $\alpha$ and $\alpha^{-1}$ stay bounded.

The new pair difference is exactly $\alpha\Delta z=A/h$. The centered coordinates of a two-body cluster with masses $p,q$ are $(-q,p)/A$ times its difference. So the centered pair $z$-coordinates are $h^{-1}(-q,p)=h^{-1}a$. For the same reason the centered pair $w$-coordinates are proportional to $a$, which gives the form $b=\beta a$. The new third centered triple $w$-coordinate is $\alpha^{-1}w_*=h\Delta z\,w_*/A=1/h$, which is the normalization $d_3=1$.

The short differences have scale $R^{-1}$: these are the pair $w$-difference and the triple $z$-differences. After division by $h$ they make $b$ and $c$ bounded. The long triple $w$-differences make $d$ bounded, with each difference bounded away from zero. The individual coordinates $d_k$ are bounded away from zero because all triple vertices are circled while their exact center is $O(R^{-2})$. The center estimates make $\eta_z$ and $\eta_w$ bounded. The pair metric is $\delta_P^2\beta A^2=1$. Since its radius has a finite nonzero limit, this makes $\beta$ bounded and bounded away from zero.

Pass to a common subsequence. All variables then converge, all internal inverse roots are finite and nonzero, and all cross roots $\rho_{ik}=\delta_{ik}/h$ are finite and nonzero. This establishes the chart and its limiting roots. The correction rates will follow from the equations; either choice of $h$ and every distance sheet remain available.

\paragraph{The exact equations in this chart.}
Write the cross inverses as $\delta_{ik}=h\rho_{ik}$. Set
\[
 \zeta_{ik}=-a_i+h^2c_k+h^3\eta_z,\qquad
 \chi_{ik}=d_k-h^2b_i+h^3\eta_w.
\]
The chart and the definition of $\eta_z,\eta_w$ give
\[
 z_i^P-z_k^T=h^{-1}a_i-hc_k-h^2\eta_z=-h^{-1}\zeta_{ik},\qquad
 w_i^P-w_k^T=hb_i-h^{-1}d_k-h^2\eta_w=-h^{-1}\chi_{ik}.
\]
In each cross metric relation $\delta_{ik}^2(z_i^P-z_k^T)(w_i^P-w_k^T)=1$, the factors $h^2$ coming from $\delta_{ik}^2=h^2\rho_{ik}^2$ and $h^{-2}$ coming from the two differences cancel. The exact cross equations are therefore
\[
 \rho_{ik}^2\zeta_{ik}\chi_{ik}=1 .
\]
Define
\[
 G_i^z=\sum_kn_k\rho_{ik}^3\zeta_{ik},\quad
 G_i^w=\sum_kn_k\rho_{ik}^3\chi_{ik},\quad
 H_k^z=\sum_ip_i\rho_{ik}^3\zeta_{ik},\quad
 H_k^w=\sum_ip_i\rho_{ik}^3\chi_{ik}.
\]
A superscript $\circ$ subtracts the appropriate cluster weighted mean. Let $F_z,F_w$ be coordinate minus internal triple force. Substitution into the original force equations gives
\begin{align}
 (1-A\delta_P^3)a_i&=-h^3(G_i^z)^\circ,&
 (1-A\delta_P^3)b_i&=-h(G_i^w)^\circ,\label{eq:d2pair}\\
 F_z(c,d)&=h(H^z)^\circ,&F_w(c,d)&=h^3(H^w)^\circ,\label{eq:d2triple}\\
 \eta_z&=\frac M{AB}\sum_{i,k}p_in_k\rho_{ik}^3\zeta_{ik},&
 \eta_w&=\frac M{AB}\sum_{i,k}p_in_k\rho_{ik}^3\chi_{ik}.
\end{align}

For example, the cross $z$-force on pair body $i$ is $-h^2G_i^z$, whereas its internal force is $A\delta_P^3h^{-1}a_i$. Subtracting the pair mean and multiplying by $h$ gives the first row of \eqref{eq:d2pair}. The pair $w$-row follows by dividing the centered equation by $h$. For the triple, the cross forces have the opposite sign; dividing by its coordinate scales $h$ and $h^{-1}$ gives \eqref{eq:d2triple}. The internal metrics are $\delta_{kl}^2(c_k-c_l)(d_k-d_l)=1$.

For the centers, weighted summation cancels internal forces and gives
\[
 AZ_P=-h^2\sum_ip_iG_i^z,\qquad
 BZ_T=h^2\sum_kn_kH_k^z.
\]
The two sums are equal. Subtraction therefore yields the displayed equation for $\eta_z$, since $A^{-1}+B^{-1}=M/(AB)$; the $w$-equation follows identically. These sums also give $AZ_P+BZ_T=AW_P+BW_T=0$.

\paragraph{The limiting potential.}
The exact potential and inertia are
\begin{align*}
 U&=pq\delta_P+\sum_{k<l}n_kn_l\delta_{kl}
       +h\sum_{i,k}p_in_k\rho_{ik},\\
 I&=\sum_ip_ia_ib_i+\sum_kn_kc_kd_k+\frac{AB}{M}h^4\eta_z\eta_w.
\end{align*}
In $I$ the mixed terms vanish because $a$, $b$, $c$ and $d$ are centered. The center contribution $AZ_PW_P+BZ_TW_T$ reduces to the last term, because $Z_P=-(B/M)h^2\eta_z$, $Z_T=(A/M)h^2\eta_z$, and similarly for $W$.

Consequently the limiting energy is the sum of the two internal potentials: $u=P_0\mu+Q$, where $P_0=pq/A^{1/3}$, $\mu^3=1$, and $Q$ is the signed normalized triple potential. The crossed contribution tends to zero. This formula is the input to the energy restriction below.

\subsection{Energy restricts the limiting triple}

Put $T=n_1n_2+n_1n_3+n_2n_3$. The inverse-cube Laplacian is
\[
 (Lv)_k=\sum_{l\ne k}n_l\delta_{kl}^3(v_k-v_l).
\]
It acts on all of $\mathbb C^3$, with $L1=0$, and it preserves the two-dimensional centered triple space. It is self-adjoint for the complex bilinear form $\langle v,w\rangle=\sum n_kv_kw_k$.

Since $F_z(c,d)=c-Lc$ and $F_w(c,d)=d-Ld$, setting $h=0$ in \eqref{eq:d2triple} gives $Lc=c$ and $Ld=d$ in the limit. Suppose first that $c$ and $d$ are independent. Then they span the centered space, so $L=I$ there. Together with $L1=0$ this gives $L=I-B^{-1}\,1\,n^{T}$ on $\mathbb C^3$. Comparing off-diagonal entries, $-n_l\delta_{kl}^3=-n_l/B$, so $\delta_{kl}^3=1/B$ on every edge. The same energy estimate applies if $c$ and $d$ are dependent but already have these equal cubes. Retaining every cube root, each $|\delta_{kl}|=B^{-1/3}$, so $|Q|\le T/B^{1/3}$.

The complete disconnected energy then lies strictly below the five-body floor:
\begin{equation}\label{eq:d2gap}
 P_0+T/B^{1/3}\le\frac{pq+T+(7/12)AB}{M^{1/3}}
             <\frac{pq+T+AB}{M^{1/3}}.
\end{equation}
To verify \eqref{eq:d2gap}, put $\theta=A/M$ and $\psi=B/M$, so that $\theta+\psi=1$. The excess of the left side over $(pq+T)/M^{1/3}$ is
\[
 M^{-1/3}\{pq(\theta^{-1/3}-1)+T(\psi^{-1/3}-1)\}.
\]
Use $pq\le A^2/4=M^2\theta^2/4$, $T\le B^2/3=M^2\psi^2/3$, and $\theta^{1/3}\ge \theta$, $\psi^{1/3}\ge \psi$. The last two give $1-\theta^{1/3}\le1-\theta=\psi$ and $1-\psi^{1/3}\le \theta$. Hence the excess is at most
\[
 M^{5/3}\{\theta^{5/3}(1-\theta^{1/3})/4+\psi^{5/3}(1-\psi^{1/3})/3\}
 \le M^{5/3}\theta\psi\{\theta^{2/3}/4+\psi^{2/3}/3\}
 \le\frac{7AB}{12M^{1/3}}.
\]
The last step uses $\theta^{2/3},\psi^{2/3}\le1$ and $M^{5/3}\theta\psi=AB/M^{1/3}$. This proves \eqref{eq:d2gap}, whose strict inequality uses $AB>0$. Since $|u|\le P_0+|Q|$, it contradicts the physical floor on every phase $\mu$.

Otherwise $c$ and $d$ are dependent, so $c=\kappa d$. Here $\kappa\ne0$, because $c=0$ is incompatible with the internal metric relations $\delta_{kl}^2(c_k-c_l)(d_k-d_l)=1$. Self-adjointness and $Lc=c$ give the triple virial
\[
 \langle c,d\rangle=\langle Lc,d\rangle
 =\sum_{k<l}n_kn_l\delta_{kl}^3(c_k-c_l)(d_k-d_l)
 =\sum_{k<l}n_kn_l\delta_{kl}=Q .
\]
If $S_d=\langle d,d\rangle=0$, then $Q=\kappa S_d=0$, and the energy is again below the floor by \eqref{eq:d2gap}. The only remaining sector is therefore the nonisotropic Euler sector with unequal inverse cubes.

\subsection{The regular response obstruction}

On this sector $Ld=d$ and $S_d\ne0$. Hence the centered space is the direct sum of the line spanned by $d$ and its bilinear orthogonal complement. That complement is one-dimensional and nonisotropic, and the self-adjoint operator $L$ preserves it. Let $\ell$ be the eigenvalue of $L$ on this transverse line.

On each local nonzero root branch, the metric derivative gives
\begin{align*}
 DF_z&=(I+L/2)\Delta c+(3\kappa L/2)\Delta d,\\
 DF_w&=(I+L/2)\Delta d+(3L/(2\kappa))\Delta c.
\end{align*}
Indeed, differentiating $\delta_{kl}^2(c_k-c_l)(d_k-d_l)=1$ and using $c=\kappa d$ gives
\[
 D\delta_{kl}=-\frac{\delta_{kl}}2
 \left(\frac{\Delta c_k-\Delta c_l}{\kappa(d_k-d_l)}
       +\frac{\Delta d_k-\Delta d_l}{d_k-d_l}\right).
\]
Then $-3\sum_ln_l\delta_{kl}^2D\delta_{kl}(c_k-c_l)=\tfrac32(L\Delta c+\kappa L\Delta d)_k$. Adding $\Delta c-L\Delta c$ gives the first row; the second row is obtained in the same way.

On the transverse line both operators act by scalars. The determinant there is
\[
 (1+\ell/2)^2-\tfrac94\ell^2=(1-\ell)(1+2\ell).
\]
On the $d$-line we have $L=1$, and the block has rows $(3/2,\,3\kappa/2)$ and $(3/(2\kappa),\,3/2)$. Its only kernel is the reciprocal rotation $(\Delta c,\Delta d)=(\kappa d,-d)$, which is removed by $d_3=1$.

\medskip
\paragraph{The local graph.}
We solve a subset of the force equations to obtain a local graph, then test the remaining torque equation on that graph. The first step determines the response; the second supplies the obstruction.

Assume $\ell\ne1,-1/2$. Fix the nonzero limiting metric roots. Each metric equation then determines its root as a continuously differentiable complex function near the limit, because its derivative with respect to that root is nonzero. The remaining unknowns and selected force equations are
\begin{center}
\begin{tabular}{p{53mm}p{71mm}}\toprule
Unknowns & Selected equations at fixed $h$\\\midrule
Centered $c$ and centered $d$ with $d_3=1$ (three coordinates) & The longitudinal $w$-row and both transverse rows\\
$\beta$ & One pair-long equation\\
$\eta_z,\eta_w$ & The two center equations\\\bottomrule
\end{tabular}
\end{center}
More precisely, let $d_0$ be the limiting vector $d$ and let $e$ span its bilinear orthogonal complement in the centered space. For the residuals $\mathcal F_z=F_z-h(H^z)^\circ$ and $\mathcal F_w=F_w-h^3(H^w)^\circ$, choose
\[
 \langle d_0,\mathcal F_w\rangle,\qquad
 \langle e,\mathcal F_z\rangle,\qquad
 \langle e,\mathcal F_w\rangle.
\]
Both lines are nonisotropic. The two transverse rows have the nonzero determinant computed above, while the longitudinal $w$-row has rank one. The gauge removes the sole longitudinal kernel, since the rotation direction has $\Delta d_3=-1$. These three rows therefore give an invertible derivative on the three shape coordinates.

The other diagonal blocks are also invertible. From $\delta_P^2\beta A^2=1$ and $A\delta_P^3=1$ at $h=0$, the derivative of the pair-long residual is $3/(2\beta_0)$. The center block is the identity: its other dependence on $\eta_z,\eta_w$ is multiplied by $h^3$. At $h=0$ the pair and triple equations have no center derivatives, so these blocks form a block-triangular Jacobian.

The complex implicit-function theorem gives a unique local differentiable graph over $h$. Every sufficiently late point of the extracted sequence lies in this neighborhood and satisfies the selected equations, so uniqueness places it on the graph. In particular all corrections are $O(h)$, and the pair-long equation improves the pair estimate to $\beta-\beta_0=O(h^3)$.

\paragraph{The remaining torque equation.}
 At the limit set
\[
 B_k=p\rho_{1k}+q\rho_{2k},\qquad
 H_k=B_k/d_k-B^{-1}\sum_ln_lB_l/d_l.
\]
The exact relation $\rho_{ik}^2\zeta_{ik}\chi_{ik}=1$ gives $\rho_{ik}^3\zeta_{ik}=\rho_{ik}/\chi_{ik}$. At $h=0$ we have $\chi_{ik}=d_k$, so $H_k^z=B_k/d_k$ and $H$ is the limit of $(H^z)^\circ$.

The relevant identity is the exact internal triple rotational identity
\[
 \sum_kn_k[d_kH_k^z-h^2c_kH_k^w]=0 .
\]
It is derived as follows. Self-adjointness of $L$ gives, identically,
\[
 \langle d,F_z(c,d)\rangle-\langle c,F_w(c,d)\rangle
 =\langle d,c\rangle-\langle d,Lc\rangle-\langle c,d\rangle+\langle c,Ld\rangle=0 .
\]
Insert \eqref{eq:d2triple}. The weighted means drop out against the centered vectors $c$ and $d$. Dividing by $h\ne0$ then gives the identity at every point of an actual sequence.

Letting $h\to0$ shows that the leading torque vanishes:
\[
 W=\sum_kn_kB_k=0 .
\]
Chart convergence suffices for this limit. Because $d$ is centered, $\langle d,H\rangle=W=0$.

On the local graph define the simpler residual
\[
 \mathcal W(h)=\sum_{i,k}p_i n_k \rho_{ik}(h).
\]
It is differentiable and $\mathcal W(0)=W=0$. At an actual sequence point, the exact torque and metric identities give
\[
 \mathcal W(h)=h^2\sum_{i,k}p_i n_k \rho_{ik}^3(c_k\chi_{ik}-b_i\zeta_{ik})
       +h^3\eta_w\sum_{i,k}p_i n_k \rho_{ik}^3\zeta_{ik}.
\]
Indeed, subtract $\rho_{ik}=\rho_{ik}^3\zeta_{ik}\chi_{ik}$ from the torque summand and use $d_k-\chi_{ik}=h^2b_i-h^3\eta_w$. Every factor in the two sums is bounded. Thus $\mathcal W(h_n)/h_n\to0$ along the original sequence. Since $\mathcal W(0)=0$ and $\mathcal W$ is differentiable at zero, this limit is $\mathcal W'(0)$. The required first-order compatibility condition is therefore $\mathcal W'(0)=0$.

\paragraph{The first response.}
Write $d(h)=d+hd_1+o(h)$ and $c(h)=c+hc_1+o(h)$, where the unadorned $c,d$ denote the limiting vectors. The first response of \eqref{eq:d2triple} is $DF(c_1,d_1)=(H,0)$. The full triple derivative has rank three and is annihilated by the nonzero rotational functional $(d,-c)$. Its image is therefore exactly that functional's kernel. Since $\langle d,H\rangle=0$, the target $(H,0)$ lies in the image, and solving the three selected rows also solves the fourth linearized row. Resolving the response on the transverse line by Cramer's rule gives
\[
 d_1=-\frac{3\ell H}{2\kappa(1-\ell)(1+2\ell)}+\nu d .
\]
The transverse calculation leaves the coefficient $\nu$ to be fixed by the gauge.

To compute $\mathcal W'(0)$, observe that the explicit $c,b$ dependence in the crossed metrics starts at $h^2$, and the centers enter at $h^3$. Their first derivatives therefore contribute zero. At $h=0$, differentiating the root with respect to $d_k$ gives $-\rho_{ik}/(2d_k)$. Hence
\begin{equation}\label{eq:d2response}
 0=-\tfrac12\langle H,d_1\rangle
   =\frac{3\ell\langle H,H\rangle}{4\kappa(1-\ell)(1+2\ell)}.
\end{equation}
In the first equality the weighted mean in $H$ drops out because $\sum n_kd_{1,k}=0$. In the second the gauge term $\nu d$ drops out by orthogonality.

Since $H$ lies on the nonisotropic transverse line, $\langle H,H\rangle=0$ is equivalent to $H=0$. It remains to treat $\ell=1$, which the regular argument excluded. In that case $L$ is the identity on both the $d$-line and the transverse line, so self-adjointness gives $L=I$ on the centered space. This is the equal-cube sector, already excluded. Therefore every remaining actual chart must satisfy
\begin{equation}\label{eq:d2exceptions}
 \ell=0,\qquad\text{or}\quad\ell=-1/2,\qquad\text{or}\quad H=0.
\end{equation}
This is the point where the analytic argument reduces to finite algebra. The next two subsections classify the eigenvalue alternatives; a single torque estimate then excludes both families. The final subsection treats $H=0$. The resonant value $-1/2$, where the Jacobian is singular, is treated by classification and torque rather than by the implicit-function argument.

\subsection{Classification of the exceptional eigenvalues}\label{subsec:D2eigen}

The eigenvalue conditions can be expressed through the signed Euler equation and its derivative. This converts the spectral exceptions into explicit equations in the shape and masses. Put the triple positions at $(0,1,x)$ with $x\ne0,1$, and denote their positive masses by $(a,b,c)$. For coherent signs $s_{12},s_{13},s_{23}\in\{\pm1\}$, define
\begin{align*}
 k_{12}&=s_{12},&k_{13}&=s_{13}/x^3,&k_{23}&=s_{23}/(x-1)^3,\\
 \lambda_E&=(a+b)k_{12}+c[xk_{13}+(1-x)k_{23}],\\
 E&=axk_{13}+b[k_{12}+(x-1)k_{23}]+cxk_{13}-x\lambda_E,\\
 \tau_E&=(a+b)k_{12}+(a+c)k_{13}+(b+c)k_{23}.
\end{align*}
The Euler equations are $E=0$ together with the displayed force multiplier $\lambda_E$, where $\lambda_E\ne0$. The unnormalized inverse-cube Laplacian has eigenvalues $0,\lambda_E,\lambda_E\ell$ and trace $\tau_E$. Thus $\tau_E=\lambda_E(1+\ell)$, giving $\ell=\tau_E/\lambda_E-1$.

Since $\partial_x\lambda_E=2c(k_{23}-k_{13})$, differentiation gives
\[
 E_x=-2(a+c)k_{13}-2bk_{23}-\lambda_E+2cx(k_{13}-k_{23}).
\]
Subtracting $\lambda_E-2\tau_E$ leaves
\[
 -2\lambda_E+2(a+b)k_{12}+2c[xk_{13}+(1-x)k_{23}]=0.
\]
Hence $E_x=\lambda_E-2\tau_E$. Since $\lambda_E\ne0$, $\ell=-1/2$ is equivalent to $2\tau_E=\lambda_E$, that is, to $dE/dx=0$. Consequently the resonant case $\ell=-1/2$ is characterized by a multiple root of the Euler equation.

\paragraph{The two sign orbits.}
Global sign reversal can be absorbed into the common metric scale. This leaves four classes: $+++,$ $++-,$ $+-+,$ and $+--$.

For relabeling, write the ordered sign triple as $(j,k,l)=(s_{12},s_{13},s_{23})$, using the denominators in the displayed definitions of $k_{ij}$. Swapping labels 2 and 3 and rescaling the positions gives
\[
 (a,b,c;x;j,k,l)\longmapsto(a,c,b;1/x;k,j,-l).
\]
Primes in the following identities denote evaluation at the transformed arguments. Direct substitution gives
\[
 E'=-xE,\qquad \tau_E'=x^3\tau_E,\qquad
 \lambda_E'=x^3\lambda_E+x^2E.
\]
Thus $\tau_E/\lambda_E$ is preserved on $E=0$. Similarly, the swap of labels 1 and 2 sends the data to $(b,a,c;1-x;-j,l,k)$.

After normalizing the first sign to $+1$ by common sign reversal, the 2--3 swap exchanges $+++$ and $++-$ and fixes $+--$. The 1--2 swap exchanges $+++$ and $+--$ and fixes $++-$. Both swaps fix $+-+$. Hence $+++,$ $++-,$ and $+--$ form one orbit and $+-+$ forms the other. It suffices to analyze one representative from each orbit.

\paragraph{The zero eigenvalue.} This classification admits a short explicit certificate. Define $E_0=x^2(x-1)^2E$ and $Z_0=x^3(x-1)^3(\tau_E-\lambda_E)$, so that $\ell=0$ means $Z_0=0$. Let $r_E$ and $r_Z$ be their coefficient rows in $(a,b,c)$. A positive mass vector must lie in the common kernel of these two rows. Their cross product identifies that kernel whenever the rows are independent, and its vanishing locates all possible rank drops. Expanding the coefficients gives
\[
 r_E\mathbin{\times}r_Z=F(x)(1-x,x,-1).
\]
With $s_{12}=+1$, the four scalar factors are
\[
\begin{array}{c|l}
(s_{13},s_{23})&F(x)\\\hline
(1,1)&2x^2(x-1)^3(2x^2-x+1)\\
(1,-1)&-2x^3(x-1)^3(x^2-x+2)\\
(-1,1)&2x^2(x-1)^2(x^2-x+1)^2\\
(-1,-1)&-2x^3(x-1)^2(2x^2-3x+2).
\end{array}
\]
Since $x\ne0,1$, away from these quadratic roots the matrix has rank two. Its kernel is then spanned by $(1-x,x,-1)$, which has total mass zero, contradicting positivity.

At the supported quadratic roots, reduce $Z_0$ modulo the respective quadratic. The remainders are, in the same order,
\[
 \tfrac14\{(5a-b)x+a-b+4c\},\quad
 (b-a)x+3a+2b-c,\quad
 -a-b-c,\quad
 \tfrac14\{(a-5b)x-2a+6b+4c\}.
\]
Each quadratic is irreducible over $\R$, since its discriminant is negative. A root $x$ is therefore nonreal, so the real constant and linear coefficients of the remainder must both vanish. The resulting positive ratios are, respectively:
\begin{itemize}
 \item $b=5a$, $c=a$, giving $(1,5,1)$;
 \item $b=a$, $c=5a$, giving $(1,1,5)$;
 \item none, since $-a-b-c\ne0$;
 \item $a=5b$, $c=b$, giving $(5,1,1)$.
\end{itemize}
Conversely, substitution into both original rows at those roots confirms the retained families. The rank-two case and the roots of the four displayed scalar factors exhaust the possibilities, completing the $\ell=0$ classification.

\paragraph{The resonant eigenvalue.} We now classify the multiple roots, using the orbit reduction.

For $+-+$ the cleared polynomial is
\[
 x^2(x-1)^2E=-(x^2-x+1)G,\quad
 G=a(x-1)^2(x+1)+bx^2(x-2)+c(1-2x).
\]
The cubic $G$ takes the values $G(0)=a+c>0$ and $G(1)=-b-c<0$, and its leading coefficient is $a+b>0$. These signs at 0, 1 and infinity give one root in each of $(-\infty,0)$, $(0,1)$ and $(1,\infty)$. These roots exhaust its degree and are simple. The remainder of $G$ modulo $x^2-x+1$ is $(a+b+c)(1-2x)$. This is nonzero at the roots of $x^2-x+1$, so the quadratic has no common root with $G$. Hence all roots are simple, and this class has no resonance.

For $+++$ the original quintic is
\[
 \mathcal{P}=-a(x-1)^3(x^2+x+1)-bx^2(x-2)(x^2-x+1)+c(3x^2-3x+1).
\]
$\mathcal{P}$ is positive on real $x\le1$: there the $a$- and $b$-terms are nonnegative and the $c$-term is positive. After $x=1+y$, its coefficients have exactly one sign change. By Descartes' rule this gives exactly one real root $r>1$, counted with multiplicity, so the root is simple. A multiple root must therefore be a nonreal double conjugate pair, and the leading coefficient is $-(a+b)$. Hence
\[
 \mathcal{P}=-(a+b)(x^2-v_1x+v_2)^2(x-r),\quad
 v_2>0,\quad v_1^2-4v_2<0.
\]
Normalize $a+b=1$. Comparing coefficients yields
\begin{align*}
 a&=3-r-2v_1,&c&=rv_2^2-a,\\
 F_1&=-v_1^2-2v_2-2v_1r-(2a-3)=0,\\
 F_2&=r(v_1^2+2v_2)+2v_1v_2-(2-a+3c)=0,\\
 F_3&=v_2^2+2v_1v_2r-(2a+3c)=0.
\end{align*}
For example, the relation for $c$ is the constant term, $\mathcal{P}(0)=a+c=rv_2^2$. The elimination of $F_1,F_2,F_3$ is carried out explicitly in the next subsection.

\subsection{The resonant mass ratio}\label{subsec:D2resonance}

The preceding factorization has reduced resonance to three coefficient equations. We use polynomial identities to force the remaining real root to be $2$, and then recover the mass ratio. Substituting $a=3-r-2v_1$ into $F_1=0$ gives
\[
 v_2=-rv_1+r-v_1^2/2+2v_1-3/2.
\]
Every resonant chart has $x\ne0,1$, $\lambda_E\ne0$ and $a+b>0$. Clearing the Euler denominators preserves its roots and their multiplicities, and normalizing $a+b=1$ is legitimate. After substituting $a=3-r-2v_1$ and $c=rv_2^2-a$, the three equations become $f_1=f_2=f_3=0$, with the polynomials printed in Appendix~\ref{app:resonance}.

For exclusion, it is enough to find a necessary condition on $r$ for a common zero of these equations. The appendix supplies this condition as an explicit polynomial linear combination
\[
 \mathcal{A} f_1+\mathcal{B} f_2+\mathcal{C} f_3=4(r-2)\mathcal{E}_{10}(r).
\]
All coefficients of $\mathcal{E}_{10}(1+y)$ are positive. Hence $r>1$ forces $r=2$. Two further linear combinations at $r=2$ give
\[
 v_1-v_2=0,\qquad v_2^2+2v_2-1=0.
\]
Since $v_2>0$, it follows that $v_1=v_2=\sqrt2-1$. These identities use only numerical denominators and retain every solution of the coefficient equations.

Substituting back gives $a=c=3-2\sqrt2$ and $b=2\sqrt2-2$ under $a+b=1$. After a positive common scaling, this is the mass ratio
\[
 (a,b,c)=(1,2+2\sqrt2,1).
\]
The nonreal roots satisfy $x^2-(\sqrt2-1)x+(\sqrt2-1)=0$. The direct factorization
\[
 \mathcal{P}=-(3+2\sqrt2)(x-2)
       [x^2-(\sqrt2-1)x+(\sqrt2-1)]^2
\]
checks the original quintic. Thus, up to relabeling and a common positive mass scale, this is the only resonant family. Both conjugate roots remain to be tested against torque.

\subsection{One torque estimate for both exceptional families}

It remains to test the classified shapes against the crossed metric roots. In both families the middle mass contributes a vector larger than the combined outer contributions. This gives a torque obstruction uniform over all root signs and all positive pair mass ratios. With centered $d$ normalized by $d_3=1$, the crossed metrics at $h=0$ read
\[
 qd_k\rho_{1k}^2=1,\qquad -pd_k\rho_{2k}^2=1,
\]
since $\zeta_{1k}=q$, $\zeta_{2k}=-p$ and $\chi_{ik}=d_k$ there. Choose $\sigma_k$ with $\sigma_k^2=1/d_k$. Then all roots have the form
\[
 \rho_{1k}=\epsilon_k\sigma_k/\sqrt q,\qquad
 \rho_{2k}=\ii\eta_k\sigma_k/\sqrt p,\qquad \epsilon_k,\eta_k\in\{\pm1\}.
\]
Write $A_0=\sum n_k\epsilon_k\sigma_k$ and $C_0=\sum n_k\eta_k\sigma_k$. Multiplying $W=0$ by $\sqrt p/q$ shows that the original torque requires
\[
 (p/q)^{3/2}A_0+\ii C_0=0 .
\]
Then $A_0\overline{C_0}=-\ii(q/p)^{3/2}|C_0|^2$, and hence $\operatorname{Re}(A_0\overline{C_0})=0$.

The zero-eigenvalue families are permutations of $(1,5,1)$, so we relabel the triple to put the heavy mass in the middle. This preserves the torque obstruction: a permutation reorders each sum, and rescaling all $d_k$ multiplies both sums by a common nonzero square-root factor, up to the signs already retained.

To compare the three summands, we now compute their moduli in the same centered gauge. For positions $(0,1,x)$ and masses $(a,b,c)$, put
\[
 c_*=(b+cx)/(a+b+c),\qquad d=(-c_*,1-c_*,x-c_*)/(x-c_*).
\]
The relevant moduli can be read from
\[
 |d_1|^2=\frac{|b+cx|^2}{|(a+b)x-b|^2},\qquad
 |d_2|^2=\frac{|a+c-cx|^2}{|(a+b)x-b|^2},\qquad d_3=1.
\]
For the two families below, the denominator is nonzero. Substitution of the conjugate roots gives the same moduli for either root; the coordinates and their differences are all nonzero.

Normalize the triple masses to one of the displayed ratios. Define $D=|n_2\sigma_2|=n_2/\sqrt{|d_2|}$. Thus $D$ measures the middle summand in both $A_0$ and $C_0$. In each classified family the two outer summands have modulus 1 while $D>6$:
\begin{itemize}
 \item For $(1,5,1)$, use $x=(1\pm\ii\sqrt7)/4$. Substitution gives the centered moduli $|d_1|=|d_3|=1$ and $|d_2|^2=1/8$, giving $D^2=50\sqrt2>36$.
 \item For the resonance family, use $x=(\sqrt2-1\pm\ii\sqrt{6\sqrt2-7})/2$. Substitution gives $|d_1|=|d_3|=1$, while $|d_2|^2=(5-\sqrt2)/(13+9\sqrt2)<1/4$, which gives $D>(2+2\sqrt2)\sqrt2>6$.
\end{itemize}

After multiplying $A_0$ and $C_0$ by their respective middle signs, both sums equal the same middle vector $v_*=n_2\sigma_2$ plus errors $e,f$ of modulus at most 2. Hence
\[
 \operatorname{Re}\bigl((v_*+e)\overline{(v_*+f)}\bigr)\ge D^2-4D-4>0 ,
\]
where the last inequality holds because $D>6>2+2\sqrt2$. Thus $\operatorname{Re}(A_0\overline{C_0})\ne0$. The estimate covers each of the $2^3$ choices of $(\epsilon_k)$ and each of the $2^3$ choices of $(\eta_k)$ at once. Thus all 64 crossed-root choices fail the original torque, for every positive pair mass ratio.

\subsection{Exclusion of zero transverse forcing}

The remaining alternative $H=0$ forces the three centered positions onto a common circle and makes two of their cubes equal. These restrictions reduce the Euler equations to the finite polynomial test below.

Suppose $H=0$. Then $B_k/d_k$ is independent of $k$; write $B_k=Kd_k$. The cross metrics give $B_k=\sigma_k(p\epsilon_k/\sqrt q+\ii q\eta_k/\sqrt p)$. Squaring and using $\sigma_k^2=1/d_k$,
\[
 K^2d_k^3\in\{C_+,C_-\},\qquad
 C_\pm=p^2/q-q^2/p\ \pm2\ii\sqrt{pq}.
\]
Both constants are nonzero, since their imaginary parts are $\pm2\sqrt{pq}\ne0$. In particular $K\ne0$. The two constants are complex conjugates, so they have equal modulus. Thus all $|d_k|$ agree.

The three cubes $d_k^3$ take at most two values, so two of the coordinates share a cube. These two coordinates are distinct, because all differences are nonzero. Hence their ratio is a primitive cube root of unity. After permutation and common scaling write
\[
 d=(1,\omega,y),\qquad |y|=1,\qquad \omega^2+\omega+1=0 .
\]
Centering and the original Euler equations imply
\[
 P_{s,t}(y)=y(y-\omega)^2(y-1)^2
 +(\omega-1)^2\{t(y-1)^2-\omega s(y-\omega)^2\}=0,
 \quad s,t\in\{\pm1\}.
\]

To derive this necessary solvability condition from the signed collinear Euler equations, absorb the common nonzero inverse-cube factor into a multiplier $\Lambda$, normalize the sign on edge $12$ to $+1$, and set
\[
 \gamma_{12}=(\omega-1)^{-2},\quad \gamma_{13}=s(y-1)^{-2},\quad \gamma_{23}=t(y-\omega)^{-2}.
\]
For the triple masses $(a,b,c)$, centering and the three force equations at positions $(1,\omega,y)$ give
\[
 \begin{pmatrix}
 1&\omega&y&0\\
 0&-\gamma_{12}&-\gamma_{13}&-1\\
 \gamma_{12}&0&-\gamma_{23}&-\omega\\
 \gamma_{13}&\gamma_{23}&0&-y
 \end{pmatrix}
 \begin{pmatrix}a\\b\\c\\\Lambda\end{pmatrix}=0.
\]
This vector is nonzero, because the masses are positive. Expanding the determinant along the last column gives
\[
 -(y\gamma_{12}-\omega \gamma_{13}+\gamma_{23})^2
 =-\frac{P_{s,t}(y)^2}{(\omega-1)^4(y-1)^4(y-\omega)^4}.
\]
The equality holds because $(\omega-1)^2(y-1)^2(y-\omega)^2(y\gamma_{12}-\omega \gamma_{13}+\gamma_{23})=P_{s,t}(y)$. All denominators are nonzero because the positions are distinct. Hence the displayed Euler system implies exactly the needed polynomial equation.

A unit-circle root is also a root of $P^*(y)=y^5\overline{P(1/\bar y)}$, since $1/\bar y=y$ when $|y|=1$. Appendix~\ref{sec:hcert} supplies four explicit polynomial identities. Three of them force the common-root set to be empty, and the fourth forces $y=\omega^2$.

Consider that sole possibility, $d=(1,\omega,\omega^2)$. Real centering, $a+b\omega+c\omega^2=0$, can be rewritten as $(a-c)+(b-c)\omega=0$. Since $\omega$ is nonreal, this gives equal triple masses. Then $S_d=a(1+\omega^2+\omega^4)=a(1+\omega+\omega^2)=0$, a case already excluded by the energy argument. This excludes $H=0$ in the nonisotropic sector.

\medskip
The two exceptional eigenvalue families fail the torque condition, while zero transverse forcing contradicts the energy bound. These exhaust \eqref{eq:d2exceptions}, and hence exclude D2 on every physically admissible potential level.

\section{The butterfly obstruction at D6}\label{sec:D6}

The D6 configuration has two wings sharing body~$5$. Successive orders of the same exact torque identity constrain the two wings and finally give a contradiction.

\begin{proposition}[D6 exclusion]\label{prop:D6}
No actual balanced singular sequence for fixed positive masses has diagram D6. This local exclusion requires no physical energy floor.
\end{proposition}

The expansions below are estimates along an extracted sequence. Their remainders follow from bounded scaled coordinates and nonzero limiting metric roots. After the equal-pair masses are established, the gauge parameter $t$ is comparable to $R^{-1}$. The exact torque identity is tested successively at the following orders:
\begin{center}\small
\begin{tabular}{p{18mm}p{105mm}}\toprule
Order & Consequence\\\midrule
$t$ & The crossed inverse-distance roots occur in opposite pairs.\\
$t^2$ & At least one limiting scaled coordinate of the shared vertex vanishes.\\
$t^3$ & Both limiting scaled coordinates of the shared vertex vanish.\\
$t^4$ & The torque coefficient is strictly positive, giving the contradiction.\\\bottomrule
\end{tabular}
\end{center}
Each lower-order conclusion is used before the next coefficient is evaluated.

\subsection{Reduction to equal pair masses}\label{subsec:D6equal}

The $z$-wing is $125$ with $z$-circles at $1,2$. The $w$-wing is $345$ with $w$-circles at $3,4$. The masses are
\[
 (m_1,\dots,m_5)=(p,q,a,b,c),\qquad p,q,a,b,c>0 .
\]

The circled pair in each color has distinct leading coordinates: its weighted leading center is zero, its masses are positive, and both leading coordinates are nonzero. Thus the triangle rule makes every wing edge maximal. Lemma~\ref{lem:edgescales} gives bounded wing inverse distances and short wing differences $O(R^{-1})$. Between the two outer pairs, both projected differences are $\asym R$, so the crossed radii are $\asym R$ and the crossed forces are $O(R^{-2})$.

\begin{lemma}[Short-coordinate and shared-vertex torque estimates]\label{lem:D6shared}
For arbitrary positive pair masses,
\[
 z_3,z_4,z_5,w_1,w_2,w_5=O(R^{-1}),\qquad
 W_{51},W_{52},Z_{53},Z_{54}=O(R^{-1}).
\]
Let $A_z=pZ_{51}+qZ_{52}$, $A_w=pW_{51}+qW_{52}$ be the forces on body~$5$ from the first pair, and let $B_z=aZ_{53}+bZ_{54}$, $B_w=aW_{53}+bW_{54}$ be those from the second pair. Then
\[
 A_z,A_w,B_z,B_w=O(R^{-1}),\qquad
 c\,(z_5A_w-w_5A_z)=O(R^{-2}).
\]
\end{lemma}

\begin{proof}
On a maximal $z$-edge the $w$-difference is $O(R^{-1})$ and the inverse distance is bounded. Hence its $w$-force is $O(R^{-1})$. In the $w$-equations of bodies $1$ and $2$, the internal wing forces are therefore $O(R^{-1})$ and the crossed forces are $O(R^{-2})$. This proves $w_1,w_2=O(R^{-1})$. The short difference $w_5-w_1$ then gives $w_5=O(R^{-1})$. Exchanging the colors and the pairs proves $z_3,z_4,z_5=O(R^{-1})$.

The same short-edge estimate gives the four displayed force bounds, and therefore $A_w,B_z=O(R^{-1})$. The exact body-$5$ equations now give
\[
 A_z=z_5-B_z=O(R^{-1}),\qquad
 B_w=w_5-A_w=O(R^{-1}).
\]
In particular, the shared-vertex torque can be written using only the directly estimated quantities:
\[
 c\,(z_5A_w-w_5A_z)
   =c\,(z_5A_w-w_5z_5+w_5B_z)=O(R^{-2}).
\]
\end{proof}

The global centroid relation also gives $pz_1+qz_2=O(R^{-1})$ and $aw_3+bw_4=O(R^{-1})$.

Use the exact torque identity of the upper pair $\{1,2\}$:
\[
 0=c\,(z_5A_w-w_5A_z)+\sum_{\substack{i=1,2\\ j=3,4}}m_im_j\,\delta_{ij}^3\,(z_iw_j-w_iz_j).
\]
This is the general-mass form of \eqref{eq:D6torque}. By Lemma~\ref{lem:D6shared}, its shared-vertex term is $O(R^{-2})$. Each crossed term is of order $R^{-1}$. Hence the crossed terms must cancel at order $R^{-1}$.

To make this explicit, scale the long coordinates as
\[
 z_1\sim q\alpha R,\quad z_2\sim-p\alpha R,\quad
 w_3\sim b\beta R,\quad w_4\sim-a\beta R,\qquad \alpha \beta\neq0 .
\]
The four leading crossed metrics are exactly those of the D8 crossed-sheet calculation. On these crossed pairs $z_iw_j\sim-r_{ij}^2$. The leading torque condition is therefore a nonzero common factor times
\[
 1+\upsilon_0\rho\gamma+\mathrm i\,(\tau_0\rho+\sigma_0\gamma)=0,
 \qquad\gamma=(q/p)^{3/2},\quad\rho=(b/a)^{3/2},
 \qquad\sigma_0,\tau_0,\upsilon_0\in\{\pm1\}.
\]
Since $\rho,\gamma>0$, the real part gives $\upsilon_0=-1$ and $\rho\gamma=1$. The imaginary part gives $\rho=\gamma$. Hence $\rho=\gamma=1$, as in the D8 calculation. Therefore $p=q$ and $a=b$.

From now on write $a$ for the common mass $p=q$ of bodies $1,2$, and $b$ for the common mass of bodies $3,4$. The mass vector is then $(a,a,b,b,c)$.

\subsection{An exact gauge and all limiting root choices}\label{subsec:D6gauge}

We keep the roles of~\cite{AK}: $z$-edges $12,15,25$, $w$-edges $34,35,45$, and masses $(a,a,b,b,c)$ with $a,b,c>0$. The equal-pair relations are consequences of the source equations, proved in \S\ref{subsec:D6equal}. Set
\[
 M=2a+2b+c.
\]

Put $\Delta z=z_1-z_2$ and $\Delta w=w_3-w_4$. Choose $\alpha$ with $\alpha^2=\Delta w/\Delta z$, and put $t=2/(\alpha\Delta z)$. Both differences are $\asym R$. Hence $\alpha$ and $\alpha^{-1}$ are bounded, and $|t|\asym R^{-1}$. The corresponding bounded complex rotation gives
\[
 z_1-z_2=w_3-w_4=2/t,\qquad t\neq0,\quad t\to0 .
\]
We now use this gauge in place of the balanced gauge.

Write
\begin{align*}
 z_1&=t^{-1}+tP,&z_2&=-t^{-1}+tP,&z_3&=tp_3,&z_4&=tp_4,&z_5&=tp,\\
 w_1&=tq_1,&w_2&=tq_2,&w_3&=t^{-1}+tQ,&w_4&=-t^{-1}+tQ,&w_5&=tq.
\end{align*}
All eight coefficients $P,p_3,p_4,p,Q,q_1,q_2,q$ are bounded. This follows from the short-coordinate estimates of \S\ref{subsec:D6equal} and from the pair sums, which now carry equal masses. Extract limits of these eight coefficients and of the six nonzero wing inverse distances. A subscript $0$ denotes a limit along this subsequence.

For remainder control, put $s_1=1$, $s_2=-1$, $t_3=1$, $t_4=-1$. The crossed metrics are exactly
\[
 t^2r_{ij}^2=-s_it_j+t^2F_{ij}+t^4G_{ij},\qquad
 F_{ij}=s_i(q_i-Q)-t_j(P-p_j),\qquad
 G_{ij}=(P-p_j)(q_i-Q),
\]
for $i\in\{1,2\}$ and $j\in\{3,4\}$. All $F_{ij},G_{ij}$ are bounded along the sequence. The wing metrics include
\[
 r_{12}^2=2(q_1-q_2),\qquad
 r_{15}^2=(-1+t^2(p-P))(q-q_1),\qquad
 r_{25}^2=(1+t^2(p-P))(q-q_2).
\]
The three analogous equations hold on the other wing.

The forces exerted on body~$5$ by the two wings are
\begin{align*}
 A_z&=a\delta_{15}^3(z_5-z_1)+a\delta_{25}^3(z_5-z_2),&
 A_w&=a\delta_{15}^3(w_5-w_1)+a\delta_{25}^3(w_5-w_2),\\
 B_z&=b\delta_{35}^3(z_5-z_3)+b\delta_{45}^3(z_5-z_4),&
 B_w&=b\delta_{35}^3(w_5-w_3)+b\delta_{45}^3(w_5-w_4).
\end{align*}
The exact source torque identity is
\begin{equation}\label{eq:D6torque}
 0=c\,(z_5A_w-w_5A_z)+\mathcal T,\qquad
 \mathcal T=ab\sum_{\substack{i=1,2\\j=3,4}}
                 \delta_{ij}^3(z_iw_j-w_iz_j).
\end{equation}

On the edges $13,14,23,24$, the scaled crossed metrics $t^2r_{ij}^2$ have limits $-1,1,1,-1$. Write $h_{ij,0}=\lim\delta_{ij}/t$, so that $h_{ij,0}^{-2}=-s_it_j$.

The crossed wedges are $z_iw_j-w_iz_j=s_it_j/t^2+O(1)$. The shared-vertex term is $O(t^2)$ by Lemma~\ref{lem:D6shared}. The coefficient of $t$ in $\mathcal T$ must therefore vanish. Since $ab>0$, this condition reads $\sum s_it_jh_{ij,0}^3=0$. Here $h_{13,0}^3,h_{24,0}^3$ are purely imaginary and $h_{14,0}^3,h_{23,0}^3$ are real. The condition therefore forces
\[
 \delta_{13}/t\to H,\quad\delta_{24}/t\to-H,\quad
 \delta_{14}/t\to K,\quad\delta_{23}/t\to-K,
 \qquad H^2=-1,\quad K^2=1 .
\]
By the exact metric equations, each of these convergences holds with error $O(t^2)$ for the scaled inverse, along the root branch fixed by the limit. Consequently $\mathcal T=O(t^3)$.

To identify the wing limits, multiply the $z$-equations of bodies $1$ and $2$ by $t$. The short-coordinate bounds and bounded wing inverse cubes give
\[
 1=2a\delta_{12}^3+c\delta_{15}^3+O(t^2),\qquad
 1=2a\delta_{12}^3+c\delta_{25}^3+O(t^2).
\]
Their difference, with $c>0$, shows that the two attachment inverse cubes have the same limit. Put
\[
 \delta_{15}^3,\ \delta_{25}^3\to \chi\neq0,\qquad \delta_{12}^3\to\kappa \chi,
\]
and use $v,\ell$ in the same way for the other wing. Then
\[
 (2a\kappa+c)\chi=1,\qquad(2b\ell+c)v=1,\qquad
 \kappa,\ell\in\Bigl\{\tfrac18,\,-\tfrac18,\,\tfrac{\mathrm i}{2\sqrt2},\,-\tfrac{\mathrm i}{2\sqrt2}\Bigr\}.
\]
For example, the squared-distance ratio $\xi=\lim(d_{25}/d_{15})$ satisfies
\[
 \xi^3=1,\qquad \kappa^2=[2(1+\xi)]^{-3}.
\]
Both primitive cube roots of unity and all common inverse-distance root choices are retained. The coefficients $2a\kappa+c$ and $2b\ell+c$ cannot vanish, because their products with finite limits equal $1$.

\subsection{Wing estimates and the lower-order torque conditions}\label{subsec:D6rigid}

\begin{lemma}[Wing rigidity]\label{lem:D6rigid}
\[
 \delta_{15}^3=\chi+O(t^2),\qquad\delta_{25}^3=\chi+O(t^2),\qquad
 \delta_{12}^3=\kappa \chi+O(t^2),
\]
and analogously on the second wing. Moreover, each of $q_1-q$, $q_2-q$, $p_3-p$, $p_4-p$ equals its limit plus $O(t^2)$.
\end{lemma}

\begin{proof}
The two scaled force equations in Section~\ref{subsec:D6gauge} give
\[
 \delta_{15}^3-\delta_{25}^3=O(t^2),\qquad
 2a\delta_{12}^3+c\,\delta_{15}^3=1+O(t^2).
\]

The limiting inverse cubes are nonzero, so $\delta_{25}^3/\delta_{15}^3=1+O(t^2)$. Fix the cube-root branch actually taken by the sequence. This gives $r_{25}^2/r_{15}^2=\xi+O(t^2)$.

The exact wing metrics give
\[
 r_{12}^2=2(r_{15}^2+r_{25}^2)+O(t^2),
\]
and hence $\delta_{12}^3/\delta_{15}^3=\kappa+O(t^2)$.

Substitute into the second force estimate. Since $2a\kappa+c\neq0$, we obtain the three displayed rates. The second wing is treated identically.

The wing metrics now show that $q_1-q$, $q_2-q$, $p_3-p$, $p_4-p$ equal their limits plus $O(t^2)$.
\end{proof}

\begin{lemma}[First-order drifts]\label{lem:D6drift}
Set $D=b(K^3-H^3)$ and $E=-a(H^3+K^3)$. Then
\begin{align*}
 q_j&=q_{j,0}+tD+O(t^2)\ \ (j=1,2),& q&=q_0+tD+O(t^2),\\
 p_j&=p_{j,0}+tE+O(t^2)\ \ (j=3,4),& p&=p_0+tE+O(t^2).
\end{align*}
Moreover,
\[
 A_w/t\to q_0/\kappa,\qquad B_z/t\to p_0/\ell,\qquad
 P_0=\frac{c\,p_0(\ell^{-1}-1)}{2a},\qquad
 Q_0=\frac{c\,q_0(\kappa^{-1}-1)}{2b}.
\]
\end{lemma}

\begin{proof}
Divide a small-coordinate equation by $t$. Its internal force depends only on the differences and inverse cubes controlled in Lemma~\ref{lem:D6rigid}. It is therefore its limiting constant plus $O(t^2)$.

The crossed contribution in each of the $w_1,w_2$ equations is $t\,b(K^3-H^3)+O(t^3)$. In each of the $z_3,z_4$ equations it is $-t\,a(H^3+K^3)+O(t^3)$. This gives the expansions of $q_j$ and $p_j$. The differences fixed in Lemma~\ref{lem:D6rigid} transfer them to $q$ and $p$.

The limits of $A_w/t$ and $B_z/t$, and the values of $P_0,Q_0$, follow from the wing equations and the center equations.
\end{proof}

\paragraph{A crossed-torque expansion used in both tests.}
For each crossed edge, the fixed nonzero square-root branch gives
\[
 (\delta_{ij}/t)^3=h_{ij,0}^3\Bigl(1-\frac{3t^2F_{ij}}{2(-s_it_j)}+O(t^4)\Bigr),
\]
where
\[
 h_{13,0}=H,\quad h_{14,0}=K,\quad h_{23,0}=-K,\quad h_{24,0}=-H .
\]
Multiply by the exact wedge
\[
 z_iw_j-w_iz_j=s_it_j/t^2+s_iQ+t_jP+t^2(PQ-q_ip_j).
\]
On one edge, the coefficient of $t$ in $\delta_{ij}^3(z_iw_j-w_iz_j)$ is $h_{ij,0}^3s_it_j$, and the sum of these over the four edges cancels. The coefficient of $t^3$ on one edge is
\[
 h_{ij,0}^3\bigl\{s_i(-Q/2+3q_i/2)+t_j(-P/2+3p_j/2)\bigr\}.
\]
The remainder in the inverse-cube expansion is $t^3O(t^4)$; multiplying by a wedge of order $t^{-2}$ makes it $O(t^5)$. The omitted wedge term is $O(t^2)$ and contributes $O(t^5)$ as well. These bounds hold along the fixed subsequence because the scaled coefficients are bounded. Summing the four edges therefore gives
\begin{align*}
 \mathcal T=ab\,t^3\bigl[&(H^3+K^3)\bigl(-Q+\tfrac32(q_1+q_2)\bigr)\\
                     +&(H^3-K^3)\bigl(-P+\tfrac32(p_3+p_4)\bigr)\bigr]+O(t^5).
\end{align*}

\paragraph{The second-order condition.}
By Lemma~\ref{lem:D6drift}, the $t^2$ coefficient of \eqref{eq:D6torque} is
\[
 c\,p_0q_0\,(\kappa^{-1}+\ell^{-1}-1)=0 .
\]
Both $\kappa^{-1}$ and $\ell^{-1}$ lie in $\{8,-8,2\sqrt2\,\mathrm i,-2\sqrt2\,\mathrm i\}$, and no two members of this set sum to $1$. Hence $p_0q_0=0$.

\paragraph{The third-order condition.}
Suppose $p_0=0$ and $q_0\neq0$. Wing rigidity and the drift estimates give $B_z=O(t^3)$, and the body-$5$ equation $z_5=A_z+B_z$ then gives $A_z=Et^2+O(t^3)$. Also, centering and the formula for $Q_0$ give
\[
 q_{1,0}+q_{2,0}=-\frac{cq_0}{a\kappa}.
\]
Since $z_5=Et^2+O(t^3)$, $w_5=q_0t+O(t^2)$ and $A_w=q_0t/\kappa+O(t^2)$, the shared-vertex contribution at order $t^3$ is $cEq_0(\kappa^{-1}-1)$. Centering in the $p$-coordinate gives $2aP_0+b(p_{3,0}+p_{4,0})+cp_0=0$. Since $P_0=p_0=0$ and $b>0$, it follows that $p_{3,0}+p_{4,0}=0$. Substituting these relations and the preceding coordinate sum into the crossed expansion gives the other contribution:
\[
 c q_0(H^3+K^3)\left\{\frac a2-\frac{a+3b}{2\kappa}\right\}.
\]
Using $E=-a(H^3+K^3)$, their sum is
\[
 \frac{3c\,q_0}{2}\,(H^3+K^3)\Bigl(a-\frac{a+b}{\kappa}\Bigr).
\]
Here $H^3+K^3\neq0$. The coefficient could vanish only if $\kappa=(a+b)/a>1$, which contradicts the catalogue of values of $\kappa$.

The analogous test with $q_0=0$ and $p_0\neq0$ would require $\ell=(a+b)/b>1$, which is likewise excluded.

Combined with $p_0q_0=0$, this gives $p_0=q_0=0$.

\subsection{The fourth-order contradiction}\label{subsec:D6final}

We now have $p_0=q_0=0$. The rate estimates of Lemmas~\ref{lem:D6rigid} and~\ref{lem:D6drift} give
\[
 z_5=Et^2+O(t^3),\quad w_5=Dt^2+O(t^3),\quad
 A_w,\,B_z=O(t^3),\quad A_z=Et^2+O(t^3).
\]
Centering gives
\[
 P=-\frac{2b+c}{2a}\,Et+O(t^2),\qquad
 Q=-\frac{2a+c}{2b}\,Dt+O(t^2).
\]

The shared-vertex term contributes
\[
 c\,(z_5A_w-w_5A_z)=-cDE\,t^4+O(t^5).
\]
The drift estimates give $q_1+q_2=2Dt+O(t^2)$ and $p_3+p_4=2Et+O(t^2)$. To relate these sums to the force estimates, wing rigidity gives
\[
 A_w/t=au(2q-q_1-q_2)+O(t^2),\qquad
 B_z/t=bv(2p-p_3-p_4)+O(t^2).
\]
Since $q=Dt+O(t^2)$, $p=Et+O(t^2)$ and $au,bv\ne0$, the coordinate-sum estimates are equivalent here to $A_w,B_z=O(t^3)$. The expansion of $\mathcal T$ gives
\[
 \mathcal T=ab\,t^4\Bigl[(H^3+K^3)\Bigl(\tfrac{2a+c}{2b}+3\Bigr)D+(H^3-K^3)\Bigl(\tfrac{2b+c}{2a}+3\Bigr)E\Bigr]+O(t^5).
\]

Both remainder estimates can now be read directly from the displayed formulas. In the shared-vertex term, $z_5A_w=O(t^5)$, while
\[
 w_5A_z=(Dt^2+O(t^3))(Et^2+O(t^3))=DEt^4+O(t^5).
\]
In the crossed term, replacing $P,Q,q_1+q_2,p_3+p_4$ by their linear terms costs $t^3O(t^2)=O(t^5)$, in addition to the $O(t^5)$ remainder already established above.

It remains to add the two fourth-order coefficients. Substitute
$D=-b(H^3-K^3)$ and $E=-a(H^3+K^3)$. Factoring their sum gives
\[
 -ab(H^3+K^3)(H^3-K^3)
 \left[c+\frac{2a+c}{2}+3b+\frac{2b+c}{2}+3a\right]
 =-2abM(H^6-K^6).
\]
The limiting crossed metrics give $H^6=-1$ and $K^6=1$, independently of their root signs. The exact torque identity \eqref{eq:D6torque} therefore becomes
\begin{equation}\label{eq:D6final}
 0=4abM\,t^4+O(t^5).
\end{equation}

Since $a,b,M>0$, dividing \eqref{eq:D6final} by $t^4$ and passing to the limit gives $4abM=0$, which is impossible. This proves Proposition~\ref{prop:D6}.


\section{The attached-triangle energy argument at D9}\label{sec:D9}

We work on the fixed real level $U=I=u>0$, with $Mu^3\ge S^3$.
We now prove the physical-level exclusion for the actual D9 support,
including every intermediate attachment scale. The double triangle is
$123$, the simple $w$-attachments are $14$ and $25$, and all five bodies
have $w$-circles. The internal differences and radii of the double
triangle are $\asym\eps$. In this case the complete potential must be
controlled before limits are taken.

\paragraph{Relation to AK Proposition 8.} Diagram D9 requires a separate argument from the bounded-four-product assertion in AK Proposition~8. In the D9 orders stated in their Section~8.9.2, $d_{12},d_{13},d_{23}\asym\eps^2$, $d_{14},d_{25},d_{45}\asym1$, and the four remaining distances are $\asym\eps^{-1}$. Hence $Q_{15},Q_{24}\asym\eps^{-1}$. These orders are inconsistent with the boundedness assertion for D9. We therefore treat that diagram directly on a physically admissible potential level; this observation concerns the displayed order argument and does not exhibit an actual singular sequence.


At least one attachment has $w$-difference $\asym\eps^{-2}$. Otherwise
all five $w$-coordinates would agree up to $o(\eps^{-2})$, and the
positive total mass together with the exact centroid would contradict
their circles. Pass to a common subsequence and, if necessary, apply the
arm exchange $(12)(45)$. Then exactly two order alternatives remain:
either one attachment is smaller than the maximal one, or both are
maximal. The basic stroke estimates of Section~\ref{sec:entrance} cover both alternatives throughout their full scale ranges.

We use the roles $A=\{1,2,3\}$, $p=m_4$, $q=m_5$, and
\[
 {M_A}=m_1+m_2+m_3,\quad P=p+q,\quad J=m_1m_2+m_1m_3+m_2m_3.
\]
Then $M={M_A}+P$ and $S=J+{M_A}P+pq$.

\subsection{A complete internal virial}
Let $w_A={M_A}^{-1}\sum_{i\in A}m_iw_i$ and $v_i=w_i-w_A$. Define
\[
 E_i=\sum_{a=4,5}m_a\delta_{ia}^3(z_i-z_a).
\]
Then $z_i-E_i$ is the internal $z$-force on $i\in A$. The original
equations give the exact identity
\begin{equation}\label{eq:internal}
 U_A:=\sum_{\substack{i<j\\i,j\in A}}m_im_j\delta_{ij}
     =\sum_{i\in A}m_iv_i(z_i-E_i).
\end{equation}
To see this, symmetrize the right side over the pairs of $A$. The
difference $v_i-v_j=w_i-w_j$ is paired with the internal $z$-force, and
\eqref{eq:metric} reduces each pair to $m_im_j\delta_{ij}$. Individual
terms of $U_A$ may diverge. Identity \eqref{eq:internal} controls their
sum, together with its residual, without relying on cancellation at
leading order.

\subsection{Unequal attachment scales}
Suppose attachment $14$ is smaller than the maximal attachment $25$. Set
$h=\norm{w_1-w_4}$ and $t=\norm{\delta_{14}^{-1}}$. The actual order
estimates give
\[
 \varepsilon\ll h\ll\varepsilon^{-2},\qquad
 t\asymp(\varepsilon^2h)^{1/3}\longrightarrow0.
\]
The metric and force identities then give
$|z_{14}|\asym t^2/h\asym(\eps^4/h)^{1/3}=o(\eps)$. The maximal
attachment satisfies $r_{25}\asym1$ and $z_{25}=O(\eps^2)$. We add
differences through the double triangle, using
$|z_{12}|,|w_{12}|\asym\eps$ and the like. This gives
\[
 |z_{24}|,|z_{34}|\asym\eps,\quad |w_{24}|,|w_{34}|\asym h,
 \quad |r_{24}|,|r_{34}|\asym(\eps h)^{1/2},
\]
\[
 |r_{15}|,|r_{35}|,|r_{45}|\asym\eps^{-1/2}.
\]
All $z$-differences are $O(\eps)$, so the exact centroid gives
$z_i=O(\eps)$ for every $i$.

Recall that $t\to0$. For the edges $24,34,25,15,35,45$, the ratios of the
other exterior inverse moduli to $|\delta_{14}|$ are bounded,
respectively, by
\[
 O((\eps/h)^{1/6}),\quad O((\eps/h)^{1/6}),\quad
 O(t),\quad O(\eps^{1/2}t),\quad O(\eps^{1/2}t),\quad O(\eps^{1/2}t).
\]
Every ratio tends to zero.

Now divide the right side of \eqref{eq:internal} by $|\delta_{14}|$.
Since $v_i=O(\eps)$ and $z_i=O(\eps)$, the free-coordinate contribution
is $O(\eps^2t)$. For the force terms, use the exact identity
\[
 |\delta_{ia}^3(z_i-z_a)|=|\delta_{ia}|/|w_i-w_a|.
\]
With $v_i=O(\eps)$, the contributions are as follows. Attachment $14$
gives $O(\eps/h)$. The terms $24$ and $34$ give $O((\eps/h)^{7/6})$.
Attachment $25$ gives $O(\eps^3t)$. The terms $15$ and $35$ give
$O(\eps^{7/2}t)$. Each of these tends to zero on the whole range
$\eps\ll h\ll\eps^{-2}$. Therefore $U_A=o(|\delta_{14}|)$. The exterior
ratios listed above then give
\[
 U=m_1p\delta_{14}+o(|\delta_{14}|),\qquad |\delta_{14}|\to\infty,
\]
which contradicts the fixed finite level. The argument also covers the
cases in which $r_{24}$ and $r_{34}$ tend to zero.

\subsection{Both attachments maximal}
Now both attachment radii are $\asym1$, and both attachment
$z$-differences are $\asym\eps^2$. Since the internal difference
satisfies $z_{12}\asym\eps$, we get $z_{45}\asym\eps$. The four far radii
$r_{15},r_{24},r_{34},r_{35}$ are $\asym\eps^{-1/2}$. By centering, every
$z_i$ is $O(\eps)$. The exterior force equations now determine the scale of the outer pair $45$.

Subtract the exterior $z$-equations of bodies $4$ and $5$. The forces
exerted by $A$ contribute $O(\eps^2)$, so
\[
 (1-P\delta_{45}^3)(z_4-z_5)=O(\eps^2).
\]
Hence $\delta_{45}^3=1/P+O(\eps)$, $r_{45}\asym1$ and
$w_{45}\asym\eps^{-1}$. By \eqref{eq:internal},
$U_A=O(\eps^2)\to0$.

To determine the other cubes, put $w_P=(pw_4+qw_5)/P$,
$H=w_P-w_A$ and $\Delta_w=w_4-w_5$. Exact centering gives
${M_A}w_A+Pw_P=0$, hence
\[
 \begin{aligned}
 w_P&={M_A}H/M, & w_A&=-PH/M,\\
 w_4&={M_A}H/M+q\Delta_w/P, & w_5&={M_A}H/M-p\Delta_w/P.
 \end{aligned}
\]
Since $\Delta_w=O(\eps^{-1})$ and $w_i-w_A=O(\eps)$ for $i\in A$, the identity
$w_1-w_4=(w_1-w_A)-H-q\Delta_w/P$ and the maximality of attachment $14$ imply
$|H|\asym\eps^{-2}$.

Divide the original $w_4$ and $w_5$ equations by $H$. The mutual-pair
contributions and the far-edge contributions tend to zero, which yields
\begin{equation}\label{eq:D9cubes}
 \delta_{14}^3\to {M_A}/(Mm_1),\qquad
 \delta_{25}^3\to {M_A}/(Mm_2),\qquad
 \delta_{45}^3\to1/P.
\end{equation}
The other four exterior inverses tend to zero. Hence these limits,
together with the vanishing of $U_A$, determine the limit of the
complete potential.

After selecting convergent root branches, the full potential limit is
\[
 u=\left(\frac {M_A}M\right)^{1/3}
       (p m_1^{2/3}\mu+q m_2^{2/3}\nu)
       +\frac{pq}{P^{1/3}}\xi,\qquad \mu^3=\nu^3=\xi^3=1.
\]
All $27$ cube-root choices are retained. Hence $\norm{u}\le {U_*}$, where
\[
 {U_*}=\left(\frac {M_A}M\right)^{1/3}(p m_1^{2/3}+q m_2^{2/3})
       +\frac{pq}{P^{1/3}}.
\]
H\"older's inequality with exponents $3$ and $3/2$, together with
$m_3>0$, gives
\[
 p m_1^{2/3}+q m_2^{2/3}<(p^3+q^3)^{1/3}{M_A}^{2/3}.
\]
The identities
\begin{align*}
 (P-pq/P)^3-(p^3+q^3)&=\frac{(pq)^2(3P^2-pq)}{P^3}>0,\\
 (1+{M_A}/(3P))^3-(1+{M_A}/P)&=\frac{{M_A}^2}{3P^2}+\frac{{M_A}^3}{27P^3}>0
\end{align*}
show that $(p^3+q^3)^{1/3}<P-pq/P$ and $(M/P)^{1/3}<1+{M_A}/(3P)$. Therefore
\[
 M^{1/3}{U_*}<{M_A}\Bigl(P-\frac{pq}P\Bigr)+pq\Bigl(1+\frac {M_A}{3P}\Bigr)
 ={M_A}P+pq-\frac{2{M_A}pq}{3P}<S,
\]
where the last inequality uses $J>0$. Thus $u^3\le {U_*}^3<S^3/M$,
contradicting \eqref{eq:floor}.

The two attachment alternatives exhaust the D9 support. The first contradicts bounded potential, and the second violates the physical lower bound. Together they exclude D9 on every physically admissible fixed level.

\section{Direct no-pole bounds for D10--D16}\label{sec:back}
\subsection{The two-triangle cases D10--D13}
The common support has double triangle $125$ and simple $w$-triangle $345$. On each simple $w$-stroke, $|W_{ij}|\asym\eps^{-2}$ and $|r_{ij}|\gtrsim\eps$, so
\[
 |z_i-z_j|=(|r_{ij}|\,|W_{ij}|)^{-1}=O(\eps).
\]
Also $|r_{ij}|^3=|w_i-w_j|/|W_{ij}|=O(1)$. These are upper bounds and include nonmaximal simple edges. The double triangle has $z$-differences $O(\eps)$ too. The triangles share vertex 5, so all projected $z$-differences are $O(\eps)$; every $w$-difference is $O(\eps^{-2})$. Consequently
\[
\begin{array}{c|c}
\text{squared distances}&\text{upper bound}\\\hline
d_{12},d_{15},d_{25}&O(\eps^2)\\
d_{34},d_{35},d_{45}&O(1)\\
d_{13},d_{14},d_{23},d_{24}&O(\eps^{-1}).
\end{array}
\]
Multiplying the four factors in each $Q_e$ gives the following exponents:
\[
\begin{array}{c|rrrrrrrrrr}
e&12&13&14&15&23&24&25&34&35&45\\\hline
Q_e=O(\eps^{\gamma_e})&2&0&0&0&0&0&0&6&0&0.
\end{array}
\]
Every exponent is nonnegative, so all four-products remain bounded in these four cases, for all positive masses and every circle subcase.

\subsection{The complete four-point cluster in D14 and D15}
Let the double $K_4$ be $A=\{1,2,3,4\}$, of mass $K$, and let $h=m_5$, $M=K+h$. Relative to its exact weighted centers write the internal coordinates as $e_i,f_i=O(\eps)$ and the exterior coordinates as $x=z_5-C_z$, $y=w_5-C_w$. Balanced bounds give $x,y=O(\eps^{-2})$. The exterior squared distances are $d_{i5}=(x-e_i)(y-f_i)$, so
\begin{equation}\label{eq:k4diff}
 d_{i5}-d_{j5}=x(f_j-f_i)+y(e_j-e_i)+e_if_i-e_jf_j=O(\eps^{-1}).
\end{equation}
We claim each $d_{i5}=O(\eps^{-1})$. Otherwise select an index and subsequence with $\eps|d_{i5}|\to\infty$. Equation~\eqref{eq:k4diff} makes all four squared distances asymptotically equal; hence all four radii escape. Put $\eta=\max_i|\delta_{i5}|^3\to0$. Centering gives $z_5=Kx/M$, $w_5=Ky/M$, so the actual fifth-body force equations give
\[
 \left(\frac KM-\sum_{i\in A}m_i\delta_{i5}^3\right)x
 =-\sum_{i\in A}m_i\delta_{i5}^3e_i,
\]
and the analogous equation for $y,f_i$. The common coefficient tends to $K/M>0$. Thus $x,y=O(\eta\eps)$, forcing $d_{i5}=O(\eps^2)$, a contradiction.

Every internal squared distance is $O(\eps^2)$. If body 5 is in the edge $e$, then $Q_e$ contains one exterior and three internal factors, giving $O(\eps^5)$. If body 5 is in the complementary triple, the product has two exterior and two internal factors, giving $O(\eps^2)$. Both tend to zero.

\subsection{D16}
All ten edges are double, so all ten squared distances are $O(\eps^2)$ and each $Q_e=O(\eps^8)\to0$. These direct arguments cover every relabeling and color orientation and do not use the bounded-product statement in AK Proposition~8.

\section{Completion of the proof}\label{sec:obligations}
\begin{proof}[Proof of Proposition~\ref{hyp:decay}]
Start with an arbitrary four-product pole on the fixed admissible level $X_{m,u}$. Section~\ref{sec:entrance} balances the original signed-complex sequence and applies the matrix-enumeration classification with its hypotheses checked. Use one common subsequence and one common relabeling throughout. The entrance estimates in that section give the hypotheses of the respective local arguments.

The local sections exclude D1--D4, D6, D8 and D9 on this level, and exclude a four-product pole in D7 and D10--D16.

The remaining case is D5. Its internal mass relation was derived from the leading equations in Section~\ref{sec:entrance}; hence the complementary pair belongs to the fixed set $\calR(m)$. Lemma~\ref{lem:d5} bounds every exterior squared distance by $o(\eps^{-1})$. Corollary~\ref{cor:d5}, applied to the complete index set of at most six factors, gives $P_m\to0$. A permutation merely permutes that complete set, so this is the product defined before the extraction. This proves the proposition for the original selected-pole sequence.
\end{proof}
\begin{proof}[Proof of Theorem~\ref{thm:main}]
Proposition~\ref{hyp:decay} holds on every physically admissible potential level. Proposition~\ref{thm:conditional} therefore gives the asserted finiteness.
\end{proof}

\section{Formal verification and author contributions}\label{sec:verification}
The Lean sources and review guide are publicly available at
\url{https://github.com/andersonwu2000/five-body-finiteness}.

The separate formal development states, for arbitrary positive labelled masses,
\begin{lstlisting}
theorem finite_physical_classes_of_five_positive_masses
    (m : Fin 5 -> Real) (hm : forall i, 0 < m i) :
    Finite (PhysicalSimilarityClass 5 m)
\end{lstlisting}
Here \code{PhysicalSimilarityClass} uses labelled configurations, includes collinear configurations, and quotients by translations, rotations, and positive scaling. The display uses ASCII in place of the original Unicode syntax.

The written proof cites the singular-diagram classification and completes the local and global arguments above. The formal development proves a corresponding classification from its force and metric definitions, together with the results used in those arguments. Appendix~\ref{app:leanmap} provides the statement index, diagram correspondence, and verification record.

\paragraph{Development and circulation.}
An earlier manuscript, together with the completed Lean formalization, was sent by email to Kuo-Chang Chen for expert feedback on October 6, 2026. Subsequent manuscript revisions expanded proof details, improved the exposition, and clarified the correspondence with the formal development. The core formal statements and proof code have remained unchanged since that circulation, apart from comments; the manuscript correspondence index and review documentation were subsequently refined.

\subsection{Author contributions and disclosure}
Chih-Yao Wu coordinated the research and preparation of the manuscript and serves as the corresponding author. AI agents produced the mathematical arguments, formalization, and manuscript drafts. An independent human expert review of the complete argument has not yet been completed. The reported symbolic checks verify finite identities; the formal verification record concerns the source project described above.


\clearpage
\appendix

\section{The resonance elimination certificate}\label{app:resonance}
We retain the coefficient variables $v_1,v_2,r$ from Section~\ref{subsec:D2resonance}. After eliminating $a,c$, the three coefficient equations are
\begin{align*}
 f_1&=-2rv_1+2r-v_1^2+4v_1-2v_2-3,\\
 f_2&=rv_1^2-3rv_2^2+2rv_2-4r+2v_1v_2-8v_1+10,\\
 f_3&=2rv_1v_2-3rv_2^2-r-2v_1+v_2^2+3.
\end{align*}
Define
\begin{align*}
 \mathcal{E}_{10}(r)={}&27r^{10}-60r^9+54r^8+104r^7-247r^6+144r^5\\
 &+78r^4-60r^3-45r^2+40r-8.
\end{align*}
The certificate is the polynomial identity
\begin{equation}\label{eq:rescertificate}
 \mathcal{A} f_1+\mathcal{B} f_2+\mathcal{C} f_3=4(r-2)\mathcal{E}_{10}(r).
\end{equation}
For each of $\mathcal{A},\mathcal{B},\mathcal{C}$, the row with index $j$ in the tables below lists the coefficients of $r^j$ in the basis $(1,v_1,v_2,v_1v_2,v_2^2)$. Thus every entry is an integer and the identity can be verified by multiplication. These are four times the coefficients used in the Lean theorem \texttt{coefficient\_elimination}.

\par\medskip\noindent\begin{minipage}{\linewidth}
\textbf{Coefficients of $\mathcal{A}$.}\par
\begin{center}\small
\begin{tabular}{r|rrrrr}\toprule
$j$&$1$&$v_1$&$v_2$&$v_1v_2$&$v_2^2$\\\midrule
10 & -27 & -27 & 54 & 0 & 0\\
9 & 267 & 78 & -210 & -9 & 18\\
8 & -561 & -75 & 252 & -60 & 108\\
7 & 292 & -89 & 484 & 87 & -252\\
6 & 1046 & 401 & -1634 & -115 & 360\\
5 & -2482 & -231 & 1646 & -251 & 334\\
4 & 961 & -68 & 1252 & 589 & -1492\\
3 & 1331 & 71 & -3656 & -414 & 1676\\
2 & -1369 & -8 & 2718 & 125 & -912\\
1 & 466 & -2 & -878 & -14 & 250\\
0 & -56 & 0 & 108 & 0 & -28\\
\bottomrule\end{tabular}\end{center}

\end{minipage}\par\medskip
\par\medskip\noindent\begin{minipage}{\linewidth}
\textbf{Coefficients of $\mathcal{B}$.}\par
\begin{center}\small
\begin{tabular}{r|rrrrr}\toprule
$j$&$1$&$v_1$&$v_2$&$v_1v_2$&$v_2^2$\\\midrule
10 & -54 & 0 & 0 & 0 & 0\\
9 & 237 & -27 & -18 & 0 & 0\\
8 & -357 & 78 & -78 & -9 & 0\\
7 & 23 & -75 & 288 & -60 & 0\\
6 & 1018 & -89 & -484 & 87 & 0\\
5 & -1546 & 401 & -50 & -115 & 0\\
4 & 630 & -231 & 1162 & -251 & 0\\
3 & 657 & -68 & -1584 & 589 & 0\\
2 & -843 & 71 & 992 & -414 & 0\\
1 & 343 & -8 & -306 & 125 & 0\\
0 & -50 & -2 & 38 & -14 & 0\\
\bottomrule\end{tabular}\end{center}

\end{minipage}\par\medskip
\par\medskip\noindent\begin{minipage}{\linewidth}
\textbf{Coefficients of $\mathcal{C}$.}\par
\begin{center}\small
\begin{tabular}{r|rrrrr}\toprule
$j$&$1$&$v_1$&$v_2$&$v_1v_2$&$v_2^2$\\\midrule
10 & 54 & 0 & 0 & 0 & 0\\
9 & -255 & 27 & 18 & 0 & 0\\
8 & 414 & -81 & 72 & 9 & 0\\
7 & -137 & 84 & -336 & 63 & 0\\
6 & -1217 & 93 & 540 & -66 & 0\\
5 & 2059 & -442 & -10 & 93 & 0\\
4 & -1595 & 565 & -1388 & 282 & 0\\
3 & -470 & -665 & 2116 & -495 & 0\\
2 & 1501 & 558 & -1404 & 249 & 0\\
1 & -780 & -230 & 446 & -42 & 0\\
0 & 132 & 36 & -56 & 0 & 0\\
\bottomrule\end{tabular}\end{center}

\end{minipage}\par\medskip
The positivity step uses
\begin{align*}
 \mathcal{E}_{10}(1+y)={}&27y^{10}+210y^9+729y^8+1616y^7+2623y^6\\
 &+3114y^5+2623y^4+1616y^3+729y^2+210y+27.
\end{align*}
Thus $f_1=f_2=f_3=0$ and $r>1$ imply $r=2$.

At $r=2$, put $g_i=f_i(v_1,v_2,2)$. The two further identities are
\begin{align*}
 v_1-v_2={}&(-v_2/7-4/21)g_1+(25v_2/42-3/7)g_2\\
 &+(-v_1/3-5v_2/7+22/21)g_3,\\
 v_2^2+2v_2-1={}&(2v_2/7-4/21)g_1+(4/7-25v_2/21)g_2\\
 &+(2v_1/3+10v_2/7-41/21)g_3.
\end{align*}
These are the identities in \texttt{coefficient\_fiber\_two}. When $v_2>0$, they give $v_1=v_2=\sqrt2-1$.

\section{Explicit certificates for the zero-response calculation}\label{sec:hcert}
Set $j=\sqrt3\,\ii$, so $j^2=-3$, and $\omega=(-1+j)/2$. For each sign pair $(s,t)$ use the polynomial $P_{s,t}$ defined in the D2 section and its coefficient-conjugate reciprocal $P_{s,t}^*$. The following tables give integer polynomials
\[
 A(y)=\sum_{k=0}^4(A_k+jB_k)y^k,\qquad
 B(y)=\sum_{k=0}^4(C_k+jD_k)y^k.
\]
Every displayed certificate is the identity $AP_{s,t}+BP_{s,t}^*=Ng$, verified simply by multiplication and $j^2=-3$. The integer $N$ is nonzero. Thus a common root must be a root of $g$. The certificates were obtained by exact symbolic arithmetic and checked by expansion.

\subsection*{Signs $(1,1)$: $N=82188$, $g=1$}
\begin{center}\small\begin{tabular}{r|rrrr}\toprule $k$&$A_k$&$B_k$&$C_k$&$D_k$\\\midrule
0 & -16851 & 6105 & 82188 & 0\\
1 & -930 & -12724 & -32109 & 17937\\
2 & -1260 & 25700 & 19476 & -7988\\
3 & -54051 & -36219 & 1608 & 9106\\
4 & 0 & 0 & -7203 & -1917\\
\bottomrule\end{tabular}\end{center}
\subsection*{Signs $(1,-1)$: $N=24624$, $g=1$}
\begin{center}\small\begin{tabular}{r|rrrr}\toprule $k$&$A_k$&$B_k$&$C_k$&$D_k$\\\midrule
0 & -1261 & -1261 & 9492 & 0\\
1 & -5694 & 0 & 1237 & -1237\\
2 & -1362 & 1362 & -1254 & -1254\\
3 & 1831 & 1831 & 1542 & 0\\
4 & -6708 & 0 & -559 & 559\\
\bottomrule\end{tabular}\end{center}
\subsection*{Signs $(-1,1)$: $N=1458$, $g=y-\omega^2$}
\begin{center}\small\begin{tabular}{r|rrrr}\toprule $k$&$A_k$&$B_k$&$C_k$&$D_k$\\\midrule
0 & -380 & 380 & -1551 & -1551\\
1 & -224 & -224 & 1742 & 0\\
2 & 2542 & 0 & -451 & 451\\
3 & -1230 & 1230 & -205 & -205\\
4 & 0 & 0 & 0 & 0\\
\bottomrule\end{tabular}\end{center}
\subsection*{Signs $(-1,-1)$: $N=82188$, $g=1$}
\begin{center}\small\begin{tabular}{r|rrrr}\toprule $k$&$A_k$&$B_k$&$C_k$&$D_k$\\\midrule
0 & 17583 & -5373 & 82188 & 0\\
1 & -930 & 12724 & -10851 & 25023\\
2 & -37920 & 13480 & -21720 & 5744\\
3 & -27303 & -45135 & 1608 & -9106\\
4 & 0 & 0 & 6477 & 2643\\
\bottomrule\end{tabular}\end{center}

The sole possible common root is $y=\omega^2$. Section~\ref{sec:D2} excludes this root by centering and the physical energy bound.

\clearpage
\section{Formal verification and statement correspondence}\label{app:leanmap}
The review package contains a single \code{Paper.lean}. Its entries follow the numbered theorems, lemmas, propositions and corollaries in this article. Each entry records the stable LaTeX label and checks the relevant declarations with \code{\#check}, which displays their complete types. Explicitly typed wrappers are also supplied for the main theorem, finite potential values and the six-factor bound. Run \texttt{lake env lean Paper.lean} from the package root after building the project.

The index locates the declarations whose hypotheses and conclusions correspond to each paper statement. Some paper lemmas combine several formal results. Lemma~\ref{lem:D6shared} follows the formal short-coordinate, short-force and exact-torque estimates, before the equal-mass conclusion.

\begingroup\small
\begin{longtable}{p{18mm}p{111mm}}\toprule
Statement & Entry and formal declarations\\\midrule\endhead
\ref{thm:main} & Main finiteness theorem. \code{finite_physical_classes_of_five_positive_masses}\\[4pt]
\ref{lem:normalization} & Positive normalization. \code{multiplier_pos}; \code{exists_positive_normalization}\\[4pt]
\ref{lem:floor} & Physical potential floor. \code{weighted_inverse_cubic}; \code{physicalPotentialLevel}\\[4pt]
\ref{lem:values} & Finite potential values. \code{finite_potential_values}\\[4pt]
\ref{lem:recovery} & Finite recovery from four-products. \code{finite_gauged_five_body_of_finite_four_products}; \code{five_body_four_product_recovery}\\[4pt]
\ref{prop:selection} & Two-selection principle. \code{finite_affine_set_of_two_selections}\\[4pt]
\ref{thm:classification} & Sixteen-diagram classification. \code{five_body_surviving_source_realization}; \code{ak_to_chang_identity}; \code{chang_to_ak_identity}; \code{chang_indices_exact_survivors}\\[4pt]
\ref{lem:edgescales} & Edge scales. \code{estimate_one}; \code{estimate_two}; \code{single_z_separations}\\[4pt]
\ref{lem:isolated} & Isolated color components. \code{coincident_component_circles_zero}; \code{matrix_isolated_force}\\[4pt]
\ref{lem:D5mass} & D5 mass relation. \code{five_body_source3_reciprocal_mass_cases}\\[4pt]
\ref{hyp:decay} & Physical-level pole decay. \code{fixed_level_decay_of_remaining_cases}; \code{provedRemainingAnalyticCases}\\[4pt]
\ref{thm:conditional} & Global reduction. \code{finite_physical_classes_of_fixed_level_decay}\\[4pt]
\ref{lem:six} & Six-factor bound. \code{completeR_card_le_six}\\[4pt]
\ref{lem:d5} & Three-point collapsing cluster. \code{norm_product_small}; \code{metric_small_of_akD5}\\[4pt]
\ref{cor:d5} & D5 product decay. \code{completeRProduct_tendsto_zero_of_chang3}\\[4pt]
\ref{prop:D6} & D6 exclusion. \code{false_of_chang19}\\[4pt]
\ref{lem:D6shared} & Short-coordinate and torque estimates before equal masses. \code{five_body_source19_small_center_and_forces}; \code{five_body_cross_torque_identity}; \code{five_body_cross_torque_bigO_square}; \code{five_body_source19_cross_torque_limit}\\[4pt]
\ref{lem:D6rigid} & Wing rigidity. \code{wing_rigidity}; \code{wing_cube_orders}\\[4pt]
\ref{lem:D6drift} & First-order drifts. \code{outer_translation_orders}; \code{all_translation_orders}; \code{internal_force_orders}\\[4pt]
\bottomrule\end{longtable}\endgroup

\clearpage\subsection*{AK and Chang diagram numbers}
The mathematical framework is that of Albouy and Kaloshin; Chang--Chen's matrix and order methods organize the classification in the formal development. Several modules formalize arguments already present in AK. For example, \code{Asymptotics/ClusterOrigin.lean} treats AK Proposition~1, restated as Chang Proposition~2.7; \code{Diagrams/TraceTwoCubic.lean} uses the torque argument of AK Proposition~4; and \code{Asymptotics/CollapsedComplement.lean} develops the distance argument of AK Section~6.1. The formal development proves these ingredients used in the five-body argument.

The formal classification starts from an actual balanced singular limit. Diagram rules and finite enumeration place it in one of twenty source orbits; four further exclusions leave sixteen. The theorem \code{five_body_surviving_source_realization} establishes this coverage from the force and metric equations. This is the enumeration and order-exclusion route used in Theorem~\ref{thm:classification}.

The formal classification and the AK classification refer to the same sixteen diagram types. The file \code{FiveBody/OrdinaryDiagramIdentity.lean} defines both encodings, a common label permutation for each diagram, and the required color exchange. Its theorems \code{ak\_to\_chang\_identity}, \code{chang\_to\_ak\_identity} and \code{chang\_indices\_exact\_survivors} verify the correspondence and equality of the survivor sets. The following table is read from its \code{changIndex} array; Chang's printed numbers are one more than the Lean indices.
\begin{center}
\begin{tabular}{c|rrrrrrrr}\toprule
AK & D1&D2&D3&D4&D5&D6&D7&D8\\
Chang & 5&18&20&6&3&19&4&7\\\midrule
AK & D9&D10&D11&D12&D13&D14&D15&D16\\
Chang &12&1&8&10&14&15&16&2\\\bottomrule
\end{tabular}
\end{center}
The source comments locate AK's list in Figure~11 and Chang's twenty-diagram list in Figure~9 (printed p.~66). The four excluded Chang numbers are $9,11,13,17$. The finite identities certify equality of the encoded diagrams; identifying those encodings with the printed figures is the accompanying source-transcription check. The actual-sequence classification is \code{ScaledZWLimit.five\_body\_surviving\_source\_realization}, which is included in the Theorem~\ref{thm:classification} entry.

\subsection*{Verification record}
On October 9, 2026, the accompanying project sources were rebuilt with Lean 4.30.0-rc2 in an empty project build directory, using the pinned dependency caches. A separate client checked the main theorem and its axiom dependencies; \texttt{Paper.lean} also passed. A fresh \texttt{leanchecker} replay of the final theorem module and its dependencies completed successfully. The inspected declarations use only \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}. The exact source manifest, dependency revisions, commands and logs for this run are retained separately; the accompanying review guide gives the commands for reproducing the checks.

\clearpage
\begin{thebibliography}{99}
\bibitem{Smale} S. Smale, \emph{Mathematical problems for the next century}, The Mathematical Intelligencer \textbf{20}(2) (1998), 7--15. \href{https://doi.org/10.1007/BF03025291}{doi:10.1007/BF03025291}.
\bibitem{AK} A. Albouy and V. Kaloshin, \emph{Finiteness of central configurations of five bodies in the plane}, Annals of Mathematics \textbf{176}(1) (2012), 535--588. \href{https://doi.org/10.4007/annals.2012.176.1.10}{doi:10.4007/annals.2012.176.1.10}.
\bibitem{HM} M. Hampton and R. Moeckel, \emph{Finiteness of relative equilibria of the four-body problem}, Inventiones Mathematicae \textbf{163} (2006), 289--312. \href{https://doi.org/10.1007/s00222-005-0461-0}{doi:10.1007/s00222-005-0461-0}.
\bibitem{CCI} K.-M. Chang and K.-C. Chen, \emph{Toward finiteness of central configurations for the planar six-body problem by symbolic computations. (I) Determine diagrams and orders}, Journal of Symbolic Computation \textbf{123} (2024), 102277. \href{https://doi.org/10.1016/j.jsc.2023.102277}{doi:10.1016/j.jsc.2023.102277}.
\bibitem{CCII} K.-M. Chang and K.-C. Chen, \emph{Toward Finiteness of Central Configurations for the Planar Six-Body Problem by Symbolic Computations. (II) Determine Mass Relations}, SIAM Journal on Applied Dynamical Systems \textbf{24}(3) (2025), 2369--2404. \href{https://doi.org/10.1137/24M1716070}{doi:10.1137/24M1716070}.
\bibitem{ChangThesis} K.-M. Chang, \emph{Toward finiteness of central configurations for the planar six-body problem by symbolic computations}, Ph.D. thesis, National Tsing Hua University, April 2023. Sections~6--7 and~10, Figure~9, and Appendices~I--II.
\bibitem{Roberts} G. E. Roberts, \emph{A continuum of relative equilibria in the five-body problem}, Physica D \textbf{127}(3--4) (1999), 141--145. \href{https://doi.org/10.1016/S0167-2789(98)00315-7}{doi:10.1016/S0167-2789(98)00315-7}.
\bibitem{YZ} X. Yu and S. Zhu, \emph{On finiteness of stationary configurations of the planar five-vortex problem}, Mathematische Annalen \textbf{392} (2025), 4023--4069. \href{https://doi.org/10.1007/s00208-025-03183-w}{doi:10.1007/s00208-025-03183-w}.
\bibitem{MZ} M. Moczurad and P. Zgliczy\'nski, \emph{Central Configurations with Unequal Masses: Finiteness in Several Exceptional Cases of Five Bodies}, preprint (2026), version~2. \href{https://arxiv.org/abs/2601.01165v2}{arXiv:2601.01165v2}.
\bibitem{Tomar} T. S. Tomar, \emph{Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean}, preprint (2026), version~2. \href{https://arxiv.org/abs/2610.13100v2}{arXiv:2610.13100v2}.
\bibitem{ChenTong} Z. Chen and Z. Tong, \emph{Finiteness of planar central configurations of five bodies for all positive masses: On Smale's sixth problem}, preprint (2026), version~3. \href{https://arxiv.org/abs/2610.16107v3}{arXiv:2610.16107v3}.
\end{thebibliography}

\end{document}