A lifted rational page descends through the antipodal cover
ProvedBirkhoffGlobalSection.lifted_rational_page_descendsLet be a continuous complete flow on a selected Levi-Civita component . Suppose the component is invariant under the antipodal map, that this map has no fixed points, and that the flow commutes with it. Let be a least-period closed orbit reaching its antipode at half-period.
If admits a lifted rational page, then it induces a rational two-disk global surface of section in the antipodal quotient:
The conclusion includes jointly continuous quotient dynamics, primeness of the half-period quotient binding, continuity of the quotient page, embedding of its interior, precisely the two-fold boundary identifications, and unbounded positive and negative return times for every nonbinding quotient trajectory. Transversality is measured on the smooth lift by the Levi-Civita Hamiltonian vector field.
This is a cover-descent lemma for the rational-page encoding used in the mission. It assumes neither a near-equal-mass restriction nor the existence of any page; it applies whenever the stated cover and page data are supplied.
import Definitions.Def_BirkhoffGlobalSection_LiftedRationalPage
namespace BirkhoffGlobalSection
/-- Descent of a smooth lifted rational two-disk, including its two-sided
return property, through the free invariant antipodal cover. -/
theorem lifted_rational_page_descends {μ c : ℝ} (φ : Flow ℝ (LeftEnergyState μ c))
(hanti : IsAntipodallyEquivariantFlow μ c φ)
(hinv : IsAntipodallyInvariantComponent μ c)
(hfree : IsAntipodallyFreeComponent μ c)
(γ : PeriodicOrbit φ) (hdouble : IsAntipodalDoubleCover φ γ)
(P : LiftedRationalPage φ γ) :
RationalDiskLikeGlobalSurfaceOfSection φ hanti γ := by sorry
end BirkhoffGlobalSection