The Exact Latent Solution of the Gravitational Three-Body Problem

We argue that every trajectory of the planar gravitational three-body problem (excluding measure-zero triple collision) admits a finite Latent representation to arbitrary accuracy — an exact, implicit, constructive encoding in Fourier space — under the global extension hypotheses stated in §11 (windowing regularity B\('\), collision regularization C\('\), and Saari-type triple-collision exclusion).

Near periodic orbit families, the trajectory is determined by a generating function \(G(z; \mathbf{v}_0)\) satisfying the Galerkin equation — Newton's law as an algebraic system in Fourier coordinates. The exact solution is \(x_i(t;\, \mathbf{v}_0) = G_i(e^{i\omega(\mathbf{v}_0) t};\, \mathbf{v}_0)\), where \(G\) is defined by an implicit algebraic system with exponential convergence. The Rational Latent Theorem closes the approximation chain: every truncation (Fourier, Taylor, Padé) targets an exact analytic object and is eliminable.

For arbitrary trajectories, two classical extensions cover the full phase space: windowed step-chaining (Painlevé analyticity gives \(\rho > 1\) per segment) and Levi-Civita regularization (\(\rho_{\text{reg}} > 1\) through collisions). The logical skeleton is: Galerkin + Painlevé + Levi-Civita + Saari \(\Rightarrow\) global Latent coverage — one new ingredient plus three classical theorems (Painlevé [12], Levi–Civita [14], Saari [10]); Sundman [1] addresses a different question (global series convergence). Here “complete” means representation existence in the Latent sense of §6–11, not a single closed-form formula for all initial data.

The information content of a periodic orbit is controlled by its topology: for braid word \(w \in F_2\), the Latent grade scales as \(O(|w|)\), with within-family correlations \(r = 0.968\)–\(1.000\) across 21 orbits from 8 topological families. A degree-3 / 18-mode truncation encodes figure-eight orbits in 7,560 real numbers (\(< 0.2\%\) error, \(28\times\) speedup), achieving in \(\sim 10^{3.9}\) coefficients what Sundman's series [1] requires \(\sim 10^{10^6}\) terms for.

The mathematical core is developed below; §9 records a Lean formalization target map (module names, theorem hooks). The cited Lean sources are not shipped in this repository snapshot — until an artifact path is published, treat formal claims as specifications aligned with the informal proofs here. In that roadmap, Levi-Civita regularization and the conditional Painlevé bound (if minimum separation \(\delta > 0\) then \(\tau_{\text{sing}} > 0\)) are the natural first formalization targets; a uniform lower bound on separation (hence on \(\tau_{\text{sing}}\)) across an entire energy shell (Extension B\('\), §11.2) and a full Mathlib proof of Saari-type triple-collision estimates remain analytic inputs for a end-