A prime quotient trajectory closes after two lifts

Proved

BirkhoffGlobalSection.antipodal_trajectory_double_lift_is_double_cover

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let a prime trajectory in the antipodal quotient have period $P$ , represented by a Levi-Civita lift $x$ with

\varphi_P(x)=-x,

and suppose no time $0<t<P$ reaches either $x$ or $-x$ . If the antipodal action is free and the flow is equivariant, traversing the trajectory twice produces a closed Levi-Civita orbit of least period $2P$ , with its antipodal point reached at half-period.

This isolates the elementary covering-space step from Birkhoff's geometric shooting theorem and from the open global-section assertion.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- A prime antipodally closed trajectory becomes a least-period closed orbit
after traversing it twice on a free Levi-Civita cover. -/
theorem antipodal_trajectory_double_lift_is_double_cover {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (hfree : IsAntipodallyFreeComponent μ c)
    (δ : AntipodalPeriodicTrajectory φ) :
    IsAntipodalDoubleCover φ
      (antipodalTrajectoryDoubleLift φ hanti δ) := by sorry

end BirkhoffGlobalSection

Source

Elementary covering-space consequence of the free antipodal double cover in Joung--van Koert, Proposition 2.4, https://arxiv.org/abs/2407.19159v3.

Read-back

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

Read-back model: OpenAI Codex. File SHA-256: a15b4e37bb4f7ae6a06d699c175a38b9a185320f0cc8e74ef5381ea6173fd054. This declaration is an admitted by sorry goal, not a proved theorem. It universally quantifies over implicit real $μ,c$ , a real flow $φ$ on the selected-component subtype, a proof that every existing antipodal pair evolves antipodally, a proof that no state equals its own negative, and an AntipodalPeriodicTrajectory $δ$ . Writing its point as $x$ and period as $P$ , the trajectory data say $P>0$ , $φ_P(x)=-x$ , and for every $0<t<P$ , $φ_t(x)$ is neither $x$ nor $-x$ . Equivariance is used by antipodalTrajectoryDoubleLift to form a PeriodicOrbit $γ$ with point $x$ , recorded period $2P$ , and $φ_{2P}(x)=x$ . The conclusion says $γ$ has no return to $x$ at any $0<t<2P$ and reaches $-x$ at half its recorded period, namely at $P$ . It does not assume global component invariance and does not assert quotient continuity, quotient primeness, geometric winding, an astronomical sign, or a page.

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