Example: masses $1,2,3,4,5$ give finitely many normalized central configurations

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement (Aristotle by Harmonic), with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may unconsciously read the intended meaning into the code. Reviewers must not treat it as an independent audit; compare it against the Lean code yourself.

Let $m_k=k+1$ for $k=0,1,2,3,4$ (so the masses are $1,2,3,4,5$, as complex numbers). The set NormalizedCC 5 m is finite: there are finitely many triples $(x,y,\delta)$ with $x,y\in\mathbb C^5$, $\delta$ a symmetric $5\times5$ complex array with zero diagonal, $\delta_{kl}^2((x_l-x_k)^2+(y_l-y_k)^2)=1$ for $k\ne l$, $x_k=\sum_{l\ne k}m_l\delta_{kl}^3(x_k-x_l)$, $y_k=\sum_{l\ne k}m_l\delta_{kl}^3(y_k-y_l)$ for every $k$, and $y_1=y_0$.