Birkhoff's disk-like global-section conjecture

Open

BirkhoffRestrictedThreeBody.birkhoff_global_section

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Fix a mass ratio $0<\mu\le\tfrac12$ and a Jacobi energy $c$ below the first critical value, in the source's convention $-c<H_\mu(L_1)$ . Let $\Sigma_{\mu,c}$ be the connected component of the Levi-Civita-regularized energy hypersurface $K_{\mu,c}^{-1}(0)$ corresponding to the primary at $q=(-\mu,0)$ .

Birkhoff's conjecture asserts that the Hamiltonian dynamics on this component admits a periodic orbit $\gamma$ that bounds a disk-like global surface of section:

\exists\gamma\subset\Sigma_{\mu,c} \quad\text{such that}\quad \gamma=\partial S, \qquad S\cong\overline{\mathbb D},

where the interior of $S$ is a local cross-section and every trajectory outside $\gamma$ intersects it at both a positive and a negative time. Thus a single disk records the global return dynamics on the bounded component.

The statement asks only for the existence of a binding periodic orbit. It does not identify that orbit with the retrograde family, since the cited source notes that basic nonperturbative properties of the retrograde orbit, including uniqueness and nondegeneracy, remain unknown.

Formalization Note. The theorem includes existence of a continuous complete real flow on the regularized component, with time derivative equal to the canonical Hamiltonian vector field. The disk is a smooth injective immersion of the closed unit disk, its boundary image equals the entire orbit set, local nonzero returns to its interior are excluded, and forward and backward intersection are quantified explicitly.

Retired. This statement used the original global-section predicate, which accidentally required analytic regularity and omitted pointwise transversality. It is replaced by BirkhoffRestrictedThreeBody.birkhoff_global_section_v2.

Preamble

import Definitions.Def_BirkhoffRestrictedThreeBody

Formal statement

namespace BirkhoffRestrictedThreeBody

/-- Birkhoff's conjecture for the planar circular restricted three-body problem. -/
theorem birkhoff_global_section (μ c : ℝ) (hμ0 : 0 < μ) (hμhalf : μ ≤ 1 / 2)
    (hc : belowFirstCriticalValue μ c) :
    ∃ φ : Flow ℝ (LeftEnergyState μ c),
      IsLeviCivitaHamiltonianFlow μ c φ ∧
      ∃ γ : PeriodicOrbit φ, DiskLikeGlobalSurfaceOfSection φ γ := by sorry

end BirkhoffRestrictedThreeBody

Source

Joung--van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, https://arxiv.org/abs/2407.19159, p. 1, Abstract and Introduction (open general-mass Birkhoff conjecture); Birkhoff, https://doi.org/10.1007/BF03015982.

Read-back

What the Lean code literally says, in plain math · gpt-5

Read-back — birkhoff_global_section. For every pair of real numbers $\mu,c$ , assuming $0<\mu\le \tfrac12$ and $-c<C_\mu$ , where

C_\mu=\inf\left\{e\in\mathbb R:\exists(q_1,q_2,p_1,p_2)\in\mathbb R^4,\ (q_1+\mu)^2+q_2^2>0,\ (q_1-1+\mu)^2+q_2^2>0,\ dH_\mu=0,\ H_\mu=e\right\}

and

H_\mu(q_1,q_2,p_1,p_2)=\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}},

there exists a continuous real flow $\phi_t$ , defined for every $t\in\mathbb R$ , on the subtype $L_{\mu,c}$ consisting of points in the connected component, within

R_{\mu,c}=\{s\in\mathbb R^4:K_{\mu,c}(s)=0\ \text{and}\ D(s)>0\},

of the point $\ell_\mu=(0,0,\sqrt{1-\mu},0)$ , where, writing $s=(z_1,z_2,w_1,w_2)$ ,

D(s)=\bigl(2(z_1^2-z_2^2)-1\bigr)^2+(4z_1z_2)^2

and

K_{\mu,c}(s)=\frac{w_1^2+w_2^2}{2}+c(z_1^2+z_2^2)-\frac{1-\mu}{2} +2(z_1^2+z_2^2)(z_1w_2-z_2w_1)-\mu(z_1w_2+z_2w_1) -\frac{\mu(z_1^2+z_2^2)}{\sqrt{D(s)}}.

The flow is required to satisfy the usual real-flow laws and continuity encoded by Flow, and, for every $s\in L_{\mu,c}$ , the derivative at $t=0$ of the underlying $\mathbb R^4$ -valued curve $t\mapsto\phi_t(s)$ exists and equals

X_K(s)=\left(\frac{\partial K_{\mu,c}}{\partial w_1}(s),\frac{\partial K_{\mu,c}}{\partial w_2}(s),-\frac{\partial K_{\mu,c}}{\partial z_1}(s),-\frac{\partial K_{\mu,c}}{\partial z_2}(s)\right),

where each displayed partial derivative is the Fréchet derivative applied to the corresponding standard coordinate vector. For this flow there exists a periodic-orbit datum $\gamma$ , consisting of a point $x_\gamma\in L_{\mu,c}$ , a real number $T_\gamma>0$ , and the equality $\phi_{T_\gamma}(x_\gamma)=x_\gamma$ ; $T_\gamma$ is not required to be the least period, and the periodic-orbit structure itself does not expressly require a nonconstant orbit. Its orbit set is the full-time range

O_\gamma=\{\phi_t(x_\gamma):t\in\mathbb R\}\subseteq\mathbb R^4,

using underlying phase-space points. There must then exist a globally defined map $P:\mathbb R^2\to\mathbb R^4$ such that, for the closed disk $\overline{\mathbb D}=\{u:u_1^2+u_2^2\le1\}$ , open disk $\mathbb D=\{u:u_1^2+u_2^2<1\}$ , and unit circle $S^1=\{u:u_1^2+u_2^2=1\}$ : $P$ is infinitely differentiable on $\overline{\mathbb D}$ in the within-set sense; $P(u)\in L_{\mu,c}$ for every $u\in\overline{\mathbb D}$ ; $P$ is injective when restricted to $\overline{\mathbb D}$ ; for every $u\in\overline{\mathbb D}$ , the full Fréchet derivative $dP_u:\mathbb R^2\to\mathbb R^4$ is injective; and the set equality $P(S^1)=O_\gamma$ holds, without any required synchronization between the circle parameter and flow time. Moreover, for every $s\in L_{\mu,c}$ whose underlying point lies in $P(\mathbb D)$ , there exists $\varepsilon>0$ such that, for every $t\in\mathbb R$ , if $|t|<\varepsilon$ and the underlying point of $\phi_t(s)$ also lies in $P(\mathbb D)$ , then $t=0$ . Finally, for every $s\in L_{\mu,c}$ whose underlying point is not in $O_\gamma$ , there separately exist a time $t_+>0$ and a time $t_-<0$ such that the underlying points of both $\phi_{t_+}(s)$ and $\phi_{t_-}(s)$ lie in $P(\mathbb D)$ . The last requirement places no condition on states in $O_\gamma$ , and the local isolation requirement places no condition on states outside $P(\mathbb D)$ . No sign or endpoint condition is imposed on $c$ beyond $-c<C_\mu$ ; no nonemptiness, lower-boundedness, attainment, or uniqueness hypothesis is supplied for the critical-value set defining $C_\mu$ , so the ordinary greatest-lower-bound interpretation is only guaranteed when that set has the corresponding properties, while the formal sInf term remains total. Likewise, real square root and division are total operations in the ambient formulas, although the collision-free conditions exclude zero Jacobi denominators when defining $C_\mu$ , and $D>0$ excludes the Levi–Civita denominator singularity on $L_{\mu,c}$ .

View graph