Exact replication and screening of tropical finiteness certificates for central configurations

Abstract

A machine record around Smale's 6th problem (finiteness of planar central configurations of the Newtonian n-body problem). Four contributions, all exact or certified: (i) an exact calibration of the Albouy-Chenciner mutual-distance equations in open tooling, including a machine rediscovery of their dimension-blindness (the regular tetrahedron coexists with the square in the equal-mass rhombus stratum of the 4-body distance system until the Cayley-Menger equation is adjoined; the square's side satisfies 32a^6 - 32a^3 + 7 = 0); (ii) the enrichment law, measured: adjoining the asymmetric (Roberts) equations and the energy-inertia relation makes the n = 3 distance ideal zero-dimensional directly, removing the coordinate-line components of the bare symmetric system; (iii) an independent exact reproduction of the Jensen-Leykin tropical prevariety certificate of generic-mass finiteness for n = 5 (arXiv:2301.02305v2): both published f-vectors match digit for digit, the pointedness of the recession cone is verified by an independent exact parser, and the published 257-component count is reproduced; and (iv) a screening study over mass-valuation families and equation-system variants at n = 4 and n = 5, which finds two new working valuation families beyond the two published, replicates generic-mass finiteness for n = 4 purely polyhedrally in seconds, and shows that removing the ten dependent symmetric Albouy-Chenciner equations destroys the certificate at every tested valuation, so the algebraically redundant equations are tropically load-bearing. Version 0.05 adds two decided experiments and a corrected account of the n = 6 tooling barrier: (v) the n = 4 equal-mass census was attempted in the torus by two independent exact formulations (enriched planar saturation; the Hampton-Moeckel z-system) and both produced zero output at mechanically enforced one-hour budgets, so the published counts remain untested by this record and counting work is redirected to mixed-volume bounding, consistent with the literature, which contains no direct algebraic solve of this census either; and (vi) a dimension calibration of the n = 4 Dziobek variety by recorded random linear sections found a sharp cost asymmetry: codimension-4 emptiness probes decide in one second each (probabilistic-exact support for dimension at most three, the value generic finiteness predicts), while codimension-3 census probes and a full Groebner staircase wall at their declared caps. The record therefore adopts cheap emptiness probes plus partial-Groebner leading-term bounds (after Dias-Pan, arXiv:1811.08681) for the upper-bound direction, with certified witness sets planned for lower bounds. Version 0.06 adds the n = 5 scaling test (EXP-011): the upper-bound toolkit validated at n = 4 walls at 10 distance variables under declared budgets (all section probes capped; the first live partial-Groebner run completed one subideal of fifteen), read as an engine fact since Dias-Pan completed the identical leading-term pattern in minutes under Singular; the declared second version of the instrument swaps the Groebner engine and lightens the subideal menu. The introduction now quotes the twenty-four unsolved six-body diagram cases verbatim from the Chang-Chen programme preprint, read from the primary source. Version 0.07 consolidates the engine round: Singular over QQ confirms the wall was an engine artifact (identical jobs at sub-second cost; an exact-reproduction control caught a lex-vs-grevlex harvester bug on its first outing, with impact audited and nothing consumed); the fifteen-product system completes a full basis in nine seconds, so the products variety has dimension EXACTLY five, matching the rank-one parametrization count; the full cut is bounded at five; and both the from-scratch and incremental Groebner routes to the expected four cap at declared budgets, handing the five-versus-four decision to certified witness sets. Version 0.08 opens a NEW front beyond replication: the two-pair symmetric stratum of the planar six-body problem (two bodies on the reflection axis, two mirror pairs), for which no published finiteness result was found. It records the exact quotient derivation (nine distances; the relation between cross-side and same-side pair distances; a closed-form pair-equality lemma with an explicitly excluded equal-heights sub-stratum; a six-equation mass-linear reduced system by symmetry), the machine stages (gauged shape dimension 4; generic rank 4 at two exact geometries; the regular hexagon verified in-stratum with symmetry-degenerated rank 3), the measured Groebner cost see-saw with a decisive modular feasibility screen, and the first PROVEN case of the fiber-dimension chain: the rank-at-most-1 locus meets the shape variety in dimension at most one, established by a complete mechanically-factored minor catalogue, a Boolean branch analysis, and exact 3-4-5 witness geometries. Remaining cases are enumerated with declared routes; no finiteness statement is claimed. The n = 6 tropical section now reports the measured four-attempt gfan 0.7 failure characterization and the validated 0.8beta relaunch. This is a replication-and-instruments record: the finiteness theorems replicated are due to Hampton-Moeckel, Albouy-Kaloshin and Jensen-Leykin, and the equal-mass censuses to Moczurad-Zgliczynski; the measurements are machine facts about known objects, stated with their provenance. Negative results are reported as absence of a certificate, never as a proof of the negation. All scripts, artifacts, hypotheses declared before each run, and verdicts including refutations: https://github.com/fsantibanezleal/CAOS_RESEARCH (problems/dynamical-systems/central-configurations).