Birkhoff's symmetric retrograde orbit

Proved

BirkhoffGlobalSection.birkhoff_retrograde_orbit_exists

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let $0<\mu<1$ and $-c<h_1(\mu)$ , and let $\varphi$ be the complete Levi-Civita Hamiltonian flow on $\Sigma_{\mu,c}$ . There are a point $x\in\Sigma_{\mu,c}$ and a period $P>0$ representing a prime noncontractible quotient trajectory: $\varphi_P(x)=-x$ , and no $0<t<P$ reaches either $x$ or $-x$ . Its Jacobi projection is $q_2$ -symmetric and, during $P$ , its position is a simple collision-free loop of winding $+1$ around the chosen primary.

Liu--Salomão Theorem 5.1, attributed there to Birkhoff, supplies a $q_2$ -symmetric retrograde orbit on each bounded regularized component for every $0<\mu<1$ and every energy below $L_1(\mu)$ . In their terminology, a retrograde orbit projects to a simple closed curve around the primary moving opposite to the rotating system. Joung--van Koert Proposition 2.4 supplies the antipodal Levi-Civita covering interpretation used in this row. The separate double-lift theorem records the passage from this quotient-period representation to a least-period closed orbit upstairs.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- Liu--Salomão, Theorem 5.1 (attributed there to Birkhoff), together with
their 2-unknotted description and the Levi-Civita covering interpretation of
Joung--van Koert, Proposition 2.4. -/
theorem birkhoff_retrograde_orbit_exists (μ c : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1)
    (hc : belowFirstCriticalValue μ c)
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hφ : IsLeviCivitaHamiltonianFlow μ c φ) :
    ∃ δ : AntipodalPeriodicTrajectory φ,
      IsGeometricBirkhoffRetrogradeTrajectory φ δ := by sorry

end BirkhoffGlobalSection

Source

Liu--Salomão, Theorem 5.1 and the 2-unknotted retrograde-orbit discussion in Section 1.3, https://arxiv.org/abs/2506.17867v2; Joung--van Koert, Proposition 2.4, https://arxiv.org/abs/2407.19159v3, for the Levi-Civita covering interpretation.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: 3a0ce5c68a0ae498955168732805a9632a59085fdd234a7f25f81892a35d0462. 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 of the selected connected component, and the hypothesis that every ambient orbit curve has derivative $X_K$ at time zero, it asserts existence of an AntipodalPeriodicTrajectory $δ$ . Thus there are a state $x$ and $P>0$ such that $φ_P(x)=-x$ and, for every $0<t<P$ , $φ_t(x)$ is neither $x$ nor $-x$ . It further requires $zNormSq(φ_t x)>0$ for every real $t$ ; Jacobi projection symmetry $(q_1,q_2,p_1,p_2)(-t)=(q_1,-q_2,-p_1,p_2)(t)$ ; injectivity on $[0,P)$ of the relative-position curve $(2(z_1^2-z_2^2),4z_1z_2)$ ; and global continuous functions $ρ>0,θ$ representing that curve in polar coordinates with $ρ(t+P)=ρ(t)$ and $θ(t+P)=θ(t)+2π$ . Here $V_μ$ is the collision-free differentiable zero-derivative Jacobi critical-value set. No antipodal equivariance of the flow, closed PeriodicOrbit, winding about the other primary, astronomical sign, page, or quotient conclusion is asserted.

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