A double lift descends to a prime quotient binding

Proved

BirkhoffGlobalSection.antipodal_double_cover_descends_to_prime_binding

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let the selected Levi-Civita component carry a free, component-preserving antipodal deck map, and let its flow commute with that map. If a lifted periodic orbit has least positive period $T$ and reaches its antipodal point at time $T/2$ , then its image in the antipodal quotient is a prime periodic orbit of period $T/2$ .

This is the formal lift-to-quotient bridge for the binding: no quotient return can occur at a time strictly between $0$ and $T/2$ . A return to the same lift would contradict minimality of $T$ ; a return to the antipodal lift would produce a lifted return at twice that time.

Preamble

import Definitions.Def_BirkhoffGlobalSection

Formal statement

namespace BirkhoffGlobalSection

/-- On a free invariant antipodal component, a least-period lifted orbit whose
half-period point is antipodal descends to a prime quotient binding. -/
theorem antipodal_double_cover_descends_to_prime_binding {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (hinv : IsAntipodallyInvariantComponent μ c)
    (hfree : IsAntipodallyFreeComponent μ c)
    (γ : PeriodicOrbit φ)
    (hdouble : IsAntipodalDoubleCover φ γ) :
    IsPrimeQuotientBinding φ 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: d733eb883f2a1c560ae8f3f55a1e604f639b84f2843e5a5387cff11722a9730a. 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 $X$ , a proof that existing antipodal pairs evolve antipodally, a proof that $X$ is invariant under negation, a proof that no $s∈X$ equals $-s$ , a PeriodicOrbit $γ$ with point $x$ , recorded period $T>0$ , and $φ_T(x)=x$ , and the hypothesis that $φ_t(x)\ne x$ for all $0<t<T$ while $φ_{T/2}(x)=-x$ . In the quotient $Q=X/(s∼s'\iff s=s'\text{ or }s=-s')$ , with descended map $\bar φ_t([s])=[φ_t(s)]$ , it concludes $\bar φ_{T/2}([x])=[x]$ and $\bar φ_t([x])\ne[x]$ for every $0<t<T/2$ . This is a least-positive-return assertion for one quotient point. It does not assert continuity of the quotient dynamics, embedding of the quotient orbit, existence of a page, or identification of the quotient with a named space.

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