Theorem 1.16(ii) — near-equal-mass rational global sections
OpenBirkhoffGlobalSection.near_equal_mass_birkhoff_rational_global_sectionThere exists such that, whenever
the complete antipodally equivariant Levi-Civita Hamiltonian flow on has a geometric Birkhoff retrograde orbit whose prime image in the antipodal quotient binds a rational two-disk global surface of section.
This is an existential single-page consequence of Liu--Salomão Theorems 5.1 and 1.16(ii). Theorem 5.1 supplies a -symmetric geometric retrograde orbit at every subcritical energy; Theorem 1.16(ii) proves, for mass ratios sufficiently close to , that every retrograde orbit in either regularized component binds a rational open book whose pages are global surfaces of section. The paper works with elliptic--hyperbolic regularization and the associated Reeb flow. A proof of this Lean row must therefore also transport the result to the Levi-Civita antipodal quotient and verify preservation under the positive time change; that bridge is not silently treated as part of the cited theorem statement.
import Definitions.Def_BirkhoffGlobalSection
namespace BirkhoffGlobalSection
/-- The existential single-page consequence of Liu--Salomão, Theorems 5.1 and
1.16(ii), transported to the Levi-Civita quotient model. A proof must include
the regularization and positive-time-change bridge between the two models. -/
theorem near_equal_mass_birkhoff_rational_global_section :
∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 / 2 ∧
∀ μ c : ℝ, 0 < μ → μ < 1 →
|μ - 1 / 2| < ε → belowFirstCriticalValue μ c →
∀ (φ : Flow ℝ (LeftEnergyState μ c)),
IsLeviCivitaHamiltonianFlow μ c φ →
∀ hanti : IsAntipodallyEquivariantFlow μ c φ,
∃ δ : AntipodalPeriodicTrajectory φ,
IsGeometricBirkhoffRetrogradeTrajectory φ δ ∧
RationalDiskLikeGlobalSurfaceOfSection φ hanti
(antipodalTrajectoryDoubleLift φ hanti δ) := by sorry
end BirkhoffGlobalSectionRead-back
What the Lean code literally says, in plain math · OpenAI Codex
Read-back model: OpenAI Codex. File SHA-256: 24fbdf7708e8cafcfb04d4e578840350bc7df7b1d9590e08a9a6ca6bbe57afe6. This declaration is an admitted by sorry goal, not a proved theorem. It asserts that there exists a real with such that, for every real satisfying , , and , and for every real flow on the subtype of the connected component of with positive second-collision distance based at , the following holds: if every ambient orbit curve has derivative at time zero, then for every proof that all existing antipodal state pairs evolve antipodally at every real time, there exists an AntipodalPeriodicTrajectory . Writing its point as and period as , this means , , and for every , is neither nor . It is geometrically retrograde in the literal sense that for every real , its Jacobi projection at is of its projection at , its chosen-primary relative-position curve is injective on , and that curve has global continuous polar functions with positive radius, radius period , and angle gain per . Let be the constructed PeriodicOrbit with point and period . The conclusion also requires the following rational-page predicate for : the component is invariant under and contains no ; the quotient has jointly continuous descended time maps satisfying time-zero identity and time-addition composition; the quotient class of returns at time and at no ; and there are a page and proof that its closed-unit-disk image lies in the component such that is , injective, and immersive on the closed disk, is outside on the open disk, the upstairs boundary image is the full orbit set of , the induced quotient page is continuous, its open-disk restriction is a topological embedding, two closed-disk parameters have the same quotient image exactly when they are equal or are antipodal boundary points, the quotient boundary image equals the quotient orbit, and every quotient state outside that orbit hits the quotient open page at times larger than every prescribed real bound and smaller than every prescribed real bound. Here is the set of collision-free differentiable zero-derivative Jacobi critical values. The declaration does not assert existence of a qualifying flow or equivariance proof, any astronomical sign inequality, a first-return map, quotient smoothness, or identification of with a named manifold.
Confirmed by the mission captain (proposal self-audit).