Complete antipodally equivariant Hamiltonian flow

Open

BirkhoffGlobalSection.leviCivita_flow_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)$ . There exists a complete continuous real flow $\varphi$ on $\Sigma_{\mu,c}$ generated by the Hamiltonian vector field of $K_{\mu,c}$ . It commutes with the antipodal deck transformation. In addition to the generator identity at time zero, every orbit curve satisfies

\frac{d}{d\tau}\varphi_\tau(s)\bigg|_{\tau=t} =X_{K_{\mu,c}}\bigl(\varphi_t(s)\bigr)

for every state $s$ and every $t\in\mathbb R$ . This isolates standard flow existence, deck equivariance, and propagation of the generator identity from the open global-section assertion.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- The regularized Hamiltonian vector field has a complete flow on the compact
subcritical component, and its generator identity holds at every time. -/
theorem leviCivita_flow_exists (μ c : ℝ)
    (hμ0 : 0 < μ) (hμ1 : μ < 1)
    (hc : belowFirstCriticalValue μ c) :
    ∃ φ : Flow ℝ (LeftEnergyState μ c),
      IsLeviCivitaHamiltonianFlow μ c φ ∧
      IsAntipodallyEquivariantFlow μ c φ ∧
      ∀ t : ℝ, ∀ s : LeftEnergyState μ c,
        HasDerivAt
          (fun τ : ℝ => ((φ τ s : LeftEnergyState μ c) : Phase))
          (hamiltonianVectorField (leviCivitaHamiltonian μ c)
            ((φ t s : LeftEnergyState μ c) : Phase)) t := by sorry

end BirkhoffGlobalSection

Source

Joung--van Koert, equation (2.2) and Proposition 2.4, https://arxiv.org/abs/2407.19159v3, together with standard smooth-ODE completeness on the compact regular component.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: a9ee6afe90a49dca54b0e0801af281f62fb8637fb5f9795b4d53d84298590cb5. This declaration is an admitted by sorry goal, not a proved theorem. For every real $μ,c$ satisfying $0<μ<1$ and $-c<\operatorname{sInf}(V_μ)$ , it asserts existence of a 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)$ . It requires, for every $s∈X$ , that the ambient curve $τ↦φ_τ(s)$ have derivative at $τ=0$ equal to $X_K(s)=(∂K/∂w_1,∂K/∂w_2,-∂K/∂z_1,-∂K/∂z_2)(s)$ ; for every real $t$ and every existing pair $s_1,s_2∈X$ with $s_2=-s_1$ , that $φ_t(s_2)=-φ_t(s_1)$ ; and, for every real $t$ and $s∈X$ , that the derivative at $τ=t$ of $τ↦φ_τ(s)$ equal $X_K(φ_t(s))$ . The last clause includes the time-zero generator formula. Here $V_μ$ is the set of collision-free differentiable zero-derivative Jacobi critical values. No uniqueness, compactness, component nonemptiness, orbit, or page is concluded; if $X$ is empty, the generator and equivariance clauses are vacuous and a flow on the empty type can satisfy the existential statement.

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