Case Study · Chapter 1 · §8
The Figure-Eight
That Gravity Drew
Three equal masses. One curve. No algebraic equation. A proof that took seven years after the discovery.
A Shape No One
Expected to Find
In 1993, Cris Moore was experimenting with equal-mass solutions to the gravitational three-body problem — three masses attracting each other under Newton's law, tracing complicated paths that weave around each other. Most solutions are chaotic. Some are periodic but inelegant. Then Moore's numerical simulation produced something unexpected: three equal masses chasing each other along a single smooth figure-eight, repeating forever.
Each mass follows the same curve, arriving at each point exactly one-third of a period after the mass ahead of it. The arrangement is called a choreography: a periodic solution in which all bodies trace the same closed path at equal time intervals. Moore found this one by numerical experiment. He could not prove it existed.
Cris Moore discovers the figure-eight choreography numerically. The solution exists in simulation — but is it a true solution to Newton's equations, or a numerical artifact?
Alain Chenciner and Richard Montgomery publish a rigorous existence proof in the Annals of Mathematics. The key tool: variational calculus — minimizing the action functional over the space of choreographic loops.
Carles Simó produces high-precision numerical data confirming the solution's properties: period, symmetry group, Fourier coefficients, and stability. The Fourier expansion is what makes the curve drawable.
No formal Lean proof of the choreography's existence. The proof requires formalizing the calculus of variations, collision-free minimizers, and Newton's gravitational law — open problems in Mathlib. The figure-eight is real; its Lean certificate does not yet exist.
Watch Gravity Draw the Figure-Eight
The left panel shows all three masses and the trail of one. The right panel shows the path traced by a single mass over one full period — the figure-eight curve itself. The Fourier expansion used here comes from Simó (2002).
Why This Curve
Cannot Have an Equation
The Gerono lemniscate is defined by x⁴ + y² = x². You can write it on a napkin. The Bernoulli lemniscate is (x²+y²)² = 2(x²−y²). Also a napkin. The analemma is x² = 4y²(1−y²). Napkin again.
The Chenciner–Montgomery curve has no such equation. It is the minimizer of an action functional over an infinite-dimensional space of loops — the unique closed path (up to scaling and rotation) on which Newton's gravitational three-body system achieves minimum action subject to choreography symmetry. That minimum exists and is collision-free, but it is not algebraic.
The hardest part of the proof is showing the minimizer has no collisions — that the three masses never occupy the same point. Chenciner and Montgomery used Marchal's theorem together with the D₆ symmetry of the solution space to rule out all possible collision types. Once collisions are excluded, the variational minimum is a genuine smooth periodic solution.
The Fourier expansion
Although no algebraic equation exists, the curve can be approximated to arbitrary precision by its Fourier series. For one of the three masses:
Only odd harmonics appear, reflecting the curve's symmetry. The leading term decays rapidly — 4 harmonics already give a visually indistinguishable approximation. The simulation above uses exactly these 4 harmonics, computed in real time.
The Properties of the Curve
In units where G=m=1 and the curve has unit scale. One mass traces the full figure-eight in this time.
Dihedral group of order 6: three rotational symmetries (120°) and three reflections. The most symmetric figure-eight known.
The curve crosses itself exactly once, at approximately (−0.206, 0) in normalized coordinates. A transverse A₁ node.
The two branches meet at approximately 60°, not 90°. This distinguishes it from the algebraic lemniscates, where branches are perpendicular.
No polynomial equation f(x,y)=0 defines this curve. It is transcendental — it cannot be the zero set of any polynomial.
Up to scaling and rotation, there is only one such choreography. It is an isolated point in the space of three-body solutions, not a member of a continuous family.
What Lean Can Prove
and What It Cannot
The four curves formalized in Chapter 1 — Gerono, Bernoulli, solar analemma, lunar analemma — all have explicit algebraic definitions that Lean can work with directly. The Chenciner–Montgomery choreography is different. Its existence proof requires mathematical infrastructure that has not yet been formalized in Mathlib.
- The Fourier approximation satisfies A₁ node conditions at the computed crossing point
- The D₆ symmetry of the Fourier expansion: if (x,y) is on the curve, so is (−x,y), (x,−y), and the 120° rotations
- The curve is closed: q(t+T) = q(t) for the Fourier truncation
- The three masses are always at distinct positions (from the truncation data)
- The Fourier truncation is a genuine figure-eight topologically
- Existence of a smooth periodic solution to the gravitational three-body equations
- The action minimizer is collision-free (requires Marchal's theorem in Lean)
- The minimizer is unique up to symmetry
- The exact Fourier series converges to the true solution
- The crossing angle is exactly arctan(√3) ≈ 60°
This is not a failure — it is an honest accounting. The distinction between what Lean has verified and what remains unverified is exactly the epistemic discipline the Principia Orthogona framework applies throughout. The choreography's existence is established mathematics; its Lean certificate is future work.
A smooth periodic choreographic solution to the gravitational 3-body problem exists, is collision-free, and traces a figure-eight with D₆ symmetry.
High-precision Fourier coefficients, period, crossing coordinates, and symmetry group confirmed numerically to machine precision.
No Mathlib formalization of the existence proof. Requires: calculus of variations, Newton's gravitational law, collision theory. Estimated years of work.
The Isolated Transcendental
and the Many Infinities
The Lissajous 2∶1 family is a continuous uncountable family parameterized by (a, b, φ). The planetary analemmas form a countable family indexed by planets. The algebraic quartics with A₁ nodes at the origin form another infinite family. All of these are families — connected, parameterized, smoothly varying.
The Chenciner–Montgomery choreography is none of these. It is isolated: a single point in the space of closed curves, not connected to any continuous family of figure-eights. You cannot deform it continuously into the Gerono lemniscate or the analemma — they live in different mathematical worlds. One is defined by a polynomial, the other by a physics variational principle.
This is what "many infinities" means in practice. The figure-eight appears in at least three structurally different types of mathematical context: algebraic (polynomial equations), trigonometric (Lissajous/Fourier families), and variational (action minimizers). Each type is itself infinite. And the types are not exhaustive — there may be others not yet recognized.
The choreography is the hardest figure-eight to find and the easiest to watch. Gravity found it before mathematics did. The proof came seven years later. Lean will come after that. But the shape was always there.
— Research log, G6 LLC · Newark NJ · 2026