Dimension-Independent Finiteness of Central Configurations for Positive Masses

We prove that for any \(N \geq 3\) bodies with positive masses in \(\mathbb{R}^d\) (\(d \geq 2\)), the number of central configurations modulo similarity is finite, resolving Smale's 6th Problem in every spatial dimension \(d \geq 2\) simultaneously. The proof is structural rather than enumerative: we complexify a hypothetical one-parameter family of central configurations into an analytic curve over \(\mathbb{C}\) and show that the full CC condition — the scalar identity \(F = \lambda\) together with the gradient identity \(G_k \equiv 0\) — cannot survive this continuation. This is the architectural core of the paper and the point of departure from the algebraic-elimination tradition (Hampton–Moeckel, Albouy–Kaloshin), whose results are restricted to the coplanar case \(d = 2\): our argument is uniform in the ambient dimension \(d\) and applies to every \(d \geq 2\) without modification.

Two identities on the complexified curve do the work. The scalar identity rules out odd-order and private even-order singularities via monodromy and divergence (Lemmas A and C). The gradient identity closes the remaining case through a gradient pole obstruction (Lemma D): at any non-cluster collision, some body has exactly one collision partner, and the stronger \(R^{-3/2}\) singularity of the gradient forces an uncancellable private pole in that body's gradient equation — a pole that level-set curves \(\{U = \lambda\}\) never face. Lemma D is the new ingredient relative to a scalar-only predecessor, which R. Moeckel showed could not rule out shared collisions because the same scalar identity holds along level-set curves. The two identities together reduce the problem to full cluster collisions (\(\geq 3\) bodies at one complex position), where the pole-cancellation conditions become overdetermined.

Cluster analysis covers all sizes: for \(m = 3\), a sign obstruction; for \(m = 4\), an algebraic resultant argument; for \(m \geq 5\), inductive self-application of the complexification–Borel–gradient machinery. No spectral gap bounds or genericity assumptions are required. The algebraic core is formalized in Lean 4 with zero sorry and 5 named axioms encoding 4 classical theorems (Borel 1897; entire-log existence; Łojasiewicz 1965; identity theorem with monodromy). The cluster isolation theorem (Proposition G) is independently formalized in Lean with zero trust debt, covering the full inductive chain from \(m = 3\) through all \(m \geq 5\).

Keywords: Central configurations, Smale's problems, \(N\)-body problem, analytic continuation, finiteness, formal verification

MSC 2020: 70F10, 70F15, 37N05, 32B20, 68V20