Birkhoff's retrograde rational global-section conjecture

Open

BirkhoffGlobalSection.birkhoff_retrograde_global_section

by Yivy Yu · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0<\mu<1$ and let the Hamiltonian energy satisfy $-c<h_1(\mu)$ . Let $\Sigma_{\mu,c}$ be the Levi-Civita component based at the collision over $q=(-\mu,0)$ , and let $\varphi$ be its complete Hamiltonian flow, commuting with the antipodal deck map. Write

Q_{\mu,c}=\Sigma_{\mu,c}/(s\sim -s).

Joung--van Koert Proposition 2.4 identifies this antipodal quotient with the corresponding Moser-regularized $\mathbb{RP}^3$ component. Lean constructs the topological quotient itself; it does not install Moser coordinates or a smooth atlas on that quotient. Antipodal equivariance makes the descended time maps representative-independent, and their flow laws and joint continuity are part of the formal target. Smoothness and transversality are stated on the Levi-Civita lift.

There exists a prime noncontractible quotient trajectory, represented by a lift $x\in\Sigma_{\mu,c}$ and a period $P>0$ , such that:

$\varphi_P(x)=-x$ , while no $0<t<P$ reaches either $x$ or $-x$ ;
its Jacobi projection is $q_2$ -symmetric, and during the period $P$ its position is a simple collision-free counterclockwise loop of winding $+1$ about the chosen primary; and
the quotient orbit binds a rational two-disk global surface of section.

Equivariance and freeness imply that traversing the trajectory twice gives a closed Levi-Civita orbit of least period $2P$ . The third clause means that there is a map $f:D^2\to Q_{\mu,c}$ with a smooth immersive Levi-Civita lift $\widetilde f:D^2\to\Sigma_{\mu,c}$ . The lifted disk is embedded, and its boundary is that full double-lifted orbit. The quotient interior is topologically embedded and disjoint from the binding. For closed-disk parameters $u,v$ , the exact fibers are

f(u)=f(v) \iff u=v\ \text{ or }\ u,v\in\partial D^2\ \text{ and }\ v=-u.

Thus the boundary is exactly a two-fold cover of the prime quotient binding. The lifted page interior is transverse to the Hamiltonian vector field, and every quotient trajectory outside the binding meets the quotient interior at arbitrarily large positive and arbitrarily large negative times.

This is an existential, one-labeled-primary formulation of Birkhoff's retrograde global-section problem. It asks for one rational page, not an entire rational open-book fibration, and it uses Birkhoff's geometric shooting notion rather than the stronger all-time astronomical inequality of Joung--van Koert.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- An existential, labeled-primary formulation of Birkhoff's retrograde-orbit
global-section problem. The rational page and all return conditions are stated
in the antipodal quotient, using a smooth Levi-Civita lift. -/
theorem birkhoff_retrograde_global_section (μ c : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1)
    (hc : belowFirstCriticalValue μ c)
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hφ : IsLeviCivitaHamiltonianFlow μ c φ)
    (hanti : IsAntipodallyEquivariantFlow μ c φ) :
    ∃ δ : AntipodalPeriodicTrajectory φ,
      IsGeometricBirkhoffRetrogradeTrajectory φ δ ∧
        RationalDiskLikeGlobalSurfaceOfSection φ hanti
          (antipodalTrajectoryDoubleLift φ hanti δ) := by sorry

end BirkhoffGlobalSection

Source

Birkhoff, The restricted problem of three bodies (1915), https://doi.org/10.1007/BF03015982; Liu--Salomão, Section 1.4, https://arxiv.org/abs/2506.17867v2. This is the universal finite-mass, all-subcritical open target for one labeled primary.

Read-back

What the Lean code literally says, in plain math · OpenAI Codex

Read-back model: OpenAI Codex. File SHA-256: 9749d638bd94f7a2f29b0482cbce942bb483b874c9b16cc702f5428ce9eade60. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ with $0<μ<1$ and $-c<\operatorname{sInf}(V_μ)$ , every real flow $φ$ on the subtype $X$ of the connected component of $K_{μ,c}=0$ with positive second-collision distance based at $(0,0,\sqrt{1-μ},0)$ , the hypothesis that every ambient orbit has derivative $X_K$ at time zero, and a proof $h$ that every existing antipodal state pair evolves antipodally for every real time, it asserts existence of an AntipodalPeriodicTrajectory $δ$ . Thus there are a state $x$ and $P>0$ with $φ_P(x)=-x$ , while $φ_t(x)$ is neither $x$ nor $-x$ for $0<t<P$ . It additionally requires $zNormSq(φ_t x)>0$ for every real $t$ , Jacobi time-reflection $(q_1,q_2,p_1,p_2)(-t)=(q_1,-q_2,-p_1,p_2)(t)$ , injectivity of chosen-primary relative position on $[0,P)$ , and a global positive-radius continuous polar lift of that curve whose angle gains $2π$ each period $P$ . For the constructed closed double lift $γ$ with point $x$ and period $2P$ , it further requires that $X$ be antipodally invariant and free; that the quotient $Q=X/(s∼s'\iff s=s'\text{ or }s=-s')$ carry jointly continuous descended time maps with identity and composition laws; that $[x]$ return at time $P$ and not earlier; and that a closed-disk lift $p$ be $C^∞$ , injective, immersive, and transverse to $X_K$ , with upstairs boundary equal to the full orbit set, continuous induced quotient page, embedded quotient interior, exact quotient fibers consisting only of identical parameters or antipodal boundary parameters, quotient boundary equal to the quotient orbit, and quotient-page hits arbitrarily far in both time directions for every nonbinding quotient state. Here $V_μ$ denotes collision-free differentiable zero-derivative Jacobi critical values. The declaration does not assert existence of the supplied flow or equivariance proof, an astronomical sign, a first-return map, quotient smoothness, or identification of $Q$ with a named manifold.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by Yivy Yu · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph