Validated retrograde and direct global sections

Open

BirkhoffGlobalSection.validated_range_retrograde_and_direct_global_sections

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let

0<\mu\leq\frac12, \qquad 2.1\leq c\leq2.1+10^{-6}.

The Levi-Civita Hamiltonian flow has a distinguished periodic orbit satisfying the strict Joung--van Koert astronomical-retrograde inequality and a distinguished direct orbit satisfying the corresponding strict negative inequality. Each orbit binds an ordinary disk-like global surface of section on the Levi-Civita component.

This is the positive-mass restriction of the global-section consequence in Joung--van Koert, Theorems 1.2 and 1.5. Their Proposition 2.2 and proof of Theorem 3.1 supply the strict astronomical sign conditions used here. The paper also includes the degenerate endpoint $\mu=0$ ; this Lean row omits that endpoint because the uniform local model defines the component inside $D>0$ , whereas the second inverse-distance singularity is removable only after specializing to zero mass. Both $c$ endpoints and both binding orbits are retained. The paper's additional action, symmetry, nondegeneracy, knot, self-linking, and index conclusions are not asserted here.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- The positive-mass part of Joung--van Koert's validated rectangle. Their
Theorems 1.2 and 1.5 give the two binding disks; Proposition 2.2 and the proof
of Theorem 3.1 verify the strict astronomical sign conditions. -/
theorem validated_range_retrograde_and_direct_global_sections (μ c : ℝ)
    (hμ0 : 0 < μ) (hμhalf : μ ≤ 1 / 2)
    (hc0 : 21 / 10 ≤ c) (hc1 : c ≤ 21 / 10 + 1 / 1000000)
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hφ : IsLeviCivitaHamiltonianFlow μ c φ) :
    ∃ γr γd : PeriodicOrbit φ,
      IsAstronomicallyRetrogradeOrbit φ γr ∧
      IsAstronomicallyDirectOrbit φ γd ∧
      DiskLikeGlobalSurfaceOfSection φ γr ∧
      DiskLikeGlobalSurfaceOfSection φ γd := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, Theorems 1.2 and 1.5, Proposition 2.2, and the proof of Theorem 3.1, https://arxiv.org/abs/2407.19159v3. The formal row is restricted to positive mass and retains both closed c endpoints.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: d4895c97f9bb9c147ec4c05782136d82b1fbdc7529a14798098f4343e193a15c. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ in the closed-sided range $0<μ≤1/2$ and $2.1≤c≤2.100001$ , every real flow $φ$ on the selected zero-energy component subtype, and the hypothesis that every ambient orbit curve has derivative $X_K$ at time zero, it asserts existence of PeriodicOrbit records $γ_r,γ_d$ , each consisting of a state, a real recorded period $T>0$ , and return at $T$ . Along $γ_r$ , for every real time, $zNormSq>0$ and $(q_1+μ)p_2-q_2p_1-μ(q_1+μ)>0$ ; along $γ_d$ , for every real time, $zNormSq>0$ and the same expression is $<0$ . For each orbit separately, there exists a total page $p:\mathbb R^2→\mathbb R^4$ that is $C^∞$ at every closed-unit-disk point, maps the closed disk into the selected component, is injective there with injective derivative, has $X_K(p(u))$ outside the derivative range for every open-disk $u$ , maps the unit circle exactly onto the orbit's all-real-time ambient range, and has the property that every nonbinding state hits the open page at some time greater than every prescribed real $R$ and at some time less than every prescribed real $R$ . The pages are separate existential witnesses. The declaration does not require antipodal equivariance, subcriticality, least recorded periods, geometric winding, a rational quotient page, a first-return map, or any relation between the two pages.

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