Continuous dynamics on the antipodal quotient

Proved

BirkhoffGlobalSection.antipodal_quotient_dynamics_continuous

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

celestial-mechanicsdynamical-systemshamiltonian-dynamics

Let the selected Levi-Civita component be invariant under its free antipodal deck map, and let a continuous real flow commute with that map. Then the representative-independent time maps induced on

Q_{\mu,c}=\Sigma_{\mu,c}/(s\sim -s)

form a jointly continuous map $\mathbb{R}\times Q_{\mu,c}\to Q_{\mu,c}$ . Its identity and composition laws are inherited from the original Flow.

This is the topological descent needed before return conditions can be interpreted as statements about a genuine quotient flow rather than unrelated time maps.

Preamble

import Definitions.Def_BirkhoffGlobalSection
import Mathlib.Topology.CompactOpen

Formal statement

namespace BirkhoffGlobalSection

/-- A continuous antipodally equivariant flow descends to a jointly continuous
real action on the free invariant antipodal quotient. -/
theorem antipodal_quotient_dynamics_continuous {μ c : ℝ}
    (φ : Flow ℝ (LeftEnergyState μ c))
    (hanti : IsAntipodallyEquivariantFlow μ c φ)
    (hinv : IsAntipodallyInvariantComponent μ c)
    (hfree : IsAntipodallyFreeComponent μ c) :
    IsContinuousQuotientDynamics φ hanti := by sorry

end BirkhoffGlobalSection

Source

Formal covering-space consequence of the antipodal equivariance in Joung--van Koert, equation (2.4) and 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: ef63da7682b4e422eb02184f71c7f1c06536a7d866faac3dca1dd0d75a470647. This declaration is an admitted by sorry goal, not a proved theorem. It universally quantifies over implicit real $μ,c$ , a real flow $φ$ on the subtype $X$ of leftEnergyComponent $μ,c$ , a proof that for every real $t$ every existing pair $s_2=-s_1$ satisfies $φ_t(s_2)=-φ_t(s_1)$ , a proof that every ambient $s$ belongs to the component exactly when $-s$ does, and a proof that no state in $X$ equals its own negative. Let $Q$ be the quotient of $X$ by $s∼s'$ when $s=s'$ or $s=-s'$ , and let $\bar φ_t([s])=[φ_t(s)]$ , whose well-definedness uses the equivariance hypothesis. The conclusion says that $(t,x)↦\bar φ_t(x)$ is jointly continuous, $\bar φ_0(x)=x$ for every $x∈Q$ , and $\bar φ_{t_1+t_2}(x)=\bar φ_{t_1}(\bar φ_{t_2}(x))$ for every real $t_1,t_2$ and $x∈Q$ . It asserts no Hamiltonian generator, nonemptiness, quotient-manifold identification, orbit, or page; on an empty $X$ , the statewise clauses are vacuous.

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