Motivation and historical timeline

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).

In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for $0\leq\mu\leq 1/2$ and $2.1\leq c\leq 2.1+10^{-6}$ (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to $1/2$, in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.

Setting

Two primaries of masses $1-\mu$ and $\mu$, with $0<\mu<1$, are fixed in rotating coordinates at $(-\mu,0)$ and $(1-\mu,0)$. For a massless particle with phase coordinates $(q_1,q_2,p_1,p_2)$, the Hamiltonian is

$$H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1 -\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}} -\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.$$

This is equation (1.1) of Joung--van Koert. Let $h_1(\mu)=H_\mu(L_1)$ be the smallest collision-free critical value, where $L_1$ lies between the primaries. The subcritical range is $H_\mu=-c<h_1(\mu)$; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).

The mission labels the primary at $(-\mu,0)$. With complex Levi-Civita variables $z=z_1+iz_2$ and $w=w_1+iw_2$, the inverse position map is $q+\mu=2z^2$, and the regularized Hamiltonian is

$$\begin{aligned} K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2} +2|z|^2(z_1w_2-z_2w_1)\\ &-\mu(z_1w_2+z_2w_1) -\frac{\mu|z|^2}{|2z^2-1|}. \end{aligned}$$

On the collision-free domain, $K_{\mu,c}=|z|^2(H_\mu+c)$, and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component $\Sigma_{\mu,c}$ is anchored at $(z,w)=(0,\sqrt{1-\mu})$. Below $h_1$, it is a star-shaped three-sphere, invariant under the free antipodal deck map $(z,w)\mapsto(-z,-w)$, and it double-covers the corresponding Moser-regularized $\mathbb{R}P^3$ component (Joung--van Koert, Proposition 2.4).

Target

For every $0<\mu<1$, every $-c<h_1(\mu)$, and every complete flow $\varphi$ on $\Sigma_{\mu,c}$ generated by $X_{K_{\mu,c}}$ and commuting with the antipodal map, prove

$$\exists\,\delta\quad \operatorname{GeometricRetrograde}(\delta)\ \land\ \operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).$$

Here $\delta$ consists of $x\in\Sigma_{\mu,c}$ and a quotient period $P>0$ with $\varphi_P(x)=-x$, with no earlier positive time reaching either $x$ or $-x$. Its physical projection is required to be a $q_2$-symmetric, simple, collision-free loop of winding $+1$ around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.

The rational page is encoded by a smooth immersive disk lift $\widetilde f:D^2\to\Sigma_{\mu,c}$. Its lift is embedded, its interior is transverse to $X_{K_{\mu,c}}$, and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).

Significance

A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.

Difficulty

Existence of a $q_2$-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every $0<\mu<1$ and every energy below $L_1(\mu)$ (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).

Formalization scope

The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.

The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.

All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.

Selected references

• G. D. Birkhoff, The restricted problem of three bodies, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. DOI.
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. arXiv:0812.4076v8.
• C. Joung and O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. arXiv:2407.19159v3.
• L. Liu and P. A. S. Salomão, Finite energy foliations and global dynamics in the restricted three-body problem, arXiv:2506.17867v2 (25 May 2026). Preprint.
• L. Liu and P. A. S. Salomão, Birkhoff conjecture and finite energy foliations in Hill's lunar problem, arXiv:2606.12912 (2026). Preprint.