A global analytic section of the mass-zero energy map

The rotating Kepler Hamiltonian admits a collision-free analytic phase-space section over every real energy. This supplies a canonical globally analytic one-variable representative for the mass-zero coefficient of any jointly analytic family.

noncomputable def LeanPool.PoincareThreeBody.globalEnergyRadius (energy : ℝ) : ℝ

A small positive radius chosen so that the remaining kinetic radicand is positive for every real energy.

Equations

• LeanPool.PoincareThreeBody.globalEnergyRadius energy = 1 / (energy ^ 2 + 2)

theorem LeanPool.PoincareThreeBody.globalEnergyRadius_pos (energy : ℝ) : 0 < globalEnergyRadius energy

theorem LeanPool.PoincareThreeBody.one_div_globalEnergyRadius (energy : ℝ) : 1 / globalEnergyRadius energy = energy ^ 2 + 2

noncomputable def LeanPool.PoincareThreeBody.globalEnergyRadicand (energy : ℝ) : ℝ

The squared shifted momentum needed to realize the prescribed energy.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.globalEnergyRadicand_pos (energy : ℝ) : 0 < globalEnergyRadicand energy

noncomputable def LeanPool.PoincareThreeBody.globalEnergySpeed (energy : ℝ) : ℝ

Positive shifted momentum along the global section.

Equations

• LeanPool.PoincareThreeBody.globalEnergySpeed energy = √(LeanPool.PoincareThreeBody.globalEnergyRadicand energy)

theorem LeanPool.PoincareThreeBody.globalEnergySpeed_sq (energy : ℝ) : globalEnergySpeed energy ^ 2 = globalEnergyRadicand energy

noncomputable def LeanPool.PoincareThreeBody.globalEnergySection (energy : ℝ) : PhaseSpace

An explicit collision-free phase point with mass-zero Hamiltonian equal to energy.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.globalEnergySection_collisionFree (energy : ℝ) : (0, globalEnergySection energy) ∈ collisionFree

theorem LeanPool.PoincareThreeBody.hamiltonian_zero_globalEnergySection (energy : ℝ) : hamiltonian 0 (globalEnergySection energy) = energy

The explicit section is a right inverse of the mass-zero Hamiltonian.

@[simp]

theorem LeanPool.PoincareThreeBody.globalEnergyRadius_neg_two : globalEnergyRadius (-2) = 1 / 6

@[simp]

theorem LeanPool.PoincareThreeBody.globalEnergyRadicand_neg_two : globalEnergyRadicand (-2) = 289 / 36

@[simp]

theorem LeanPool.PoincareThreeBody.globalEnergySpeed_neg_two : globalEnergySpeed (-2) = 17 / 6

theorem LeanPool.PoincareThreeBody.globalEnergySection_neg_two : globalEnergySection (-2) = ![0, 1 / 6, -3, 0]

A rational phase-space anchor for the global section.

theorem LeanPool.PoincareThreeBody.cartesianKeplerEnergy_globalEnergySection_neg_two : cartesianKeplerEnergy (globalEnergySection (-2)) = -3 / 2

theorem LeanPool.PoincareThreeBody.cartesianAngularAction_globalEnergySection_neg_two : cartesianAngularAction (globalEnergySection (-2)) = 1 / 2

theorem LeanPool.PoincareThreeBody.cartesianDelaunayActions_globalEnergySection_neg_two : cartesianDelaunayActions (globalEnergySection (-2)) = ![1 / √3, 1 / 2]

theorem LeanPool.PoincareThreeBody.globalEnergySection_neg_two_action_prograde : cartesianDelaunayActions (globalEnergySection (-2)) ∈ ProgradeEllipticActions

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_globalEnergySection_neg_two : eccentricityFromActions (cartesianDelaunayActions (globalEnergySection (-2))) = 1 / 2

theorem LeanPool.PoincareThreeBody.globalEnergySection_neg_two_action_apoapsis : have action := cartesianDelaunayActions (globalEnergySection (-2)); action 0 ^ 2 * (1 + eccentricityFromActions action) < 1

theorem LeanPool.PoincareThreeBody.globalEnergySection_neg_two_eq_liftedDelaunayPhasePoint : globalEnergySection (-2) = liftedDelaunayPhasePoint (1 / √3) (1 / 2) 0 (Real.pi / 2)

The rational anchor is the periapsis point of the explicit interior Delaunay ellipse with L = 1 / √3, eccentricity 1/2, and apsidal angle π/2.

theorem LeanPool.PoincareThreeBody.analyticAt_globalEnergyRadius (energy : ℝ) : AnalyticAt ℝ globalEnergyRadius energy

theorem LeanPool.PoincareThreeBody.analyticAt_globalEnergyRadicand (energy : ℝ) : AnalyticAt ℝ globalEnergyRadicand energy

theorem LeanPool.PoincareThreeBody.analyticAt_globalEnergySpeed (energy : ℝ) : AnalyticAt ℝ globalEnergySpeed energy

theorem LeanPool.PoincareThreeBody.analyticAt_globalEnergySection (energy : ℝ) : AnalyticAt ℝ globalEnergySection energy

noncomputable def LeanPool.PoincareThreeBody.globalEnergyCoefficient (F : ℝ → PhaseSpace → ℝ) (energy : ℝ) : ℝ

Evaluate the mass-zero coefficient along the global energy section.

Equations

• LeanPool.PoincareThreeBody.globalEnergyCoefficient F energy = F 0 (LeanPool.PoincareThreeBody.globalEnergySection energy)

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.globalEnergyCoefficient_neg_two_eq_leadingActionCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) : globalEnergyCoefficient F (-2) = leadingActionCoefficient F ![1 / √3, angularActionFromEccentricity (1 / √3) (1 / 2)]

At the rational anchor, the global energy representative agrees with the Delaunay action representative used by the classical Poincaré-set obstruction.

theorem LeanPool.PoincareThreeBody.eventually_globalEnergySection_interiorPrograde : ∀ᶠ (energy : ℝ) in nhds (-2), have action := cartesianDelaunayActions (globalEnergySection energy); action ∈ ProgradeEllipticActions ∧ action 0 ^ 2 * (1 + eccentricityFromActions action) < 1

Energies near the rational anchor remain in the same interior prograde Delaunay chart.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_globalEnergyCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (energy : ℝ) : AnalyticAt ℝ (globalEnergyCoefficient F) energy

Joint analyticity makes the global energy representative analytic at every real energy.

def LeanPool.PoincareThreeBody.GlobalZerothCoefficientFactorization : Prop

Intrinsic form of the classical zeroth-coefficient conclusion: the coefficient at a phase point equals its value on the canonical section at the same Kepler energy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PoincareThreeBody.globalEnergyDefect (F : ℝ → PhaseSpace → ℝ) (state : PhaseSpace) : ℝ

Difference between the mass-zero coefficient and its value on the canonical section at the same Kepler energy.

Equations

• LeanPool.PoincareThreeBody.globalEnergyDefect F state = F 0 state - LeanPool.PoincareThreeBody.globalEnergyCoefficient F (LeanPool.PoincareThreeBody.hamiltonian 0 state)

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticOnNhd_globalEnergyDefect {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) : AnalyticOnNhd ℝ (globalEnergyDefect F) massZeroCollisionFree

The global energy defect is analytic throughout the mass-zero collision-free phase domain.

def LeanPool.PoincareThreeBody.LocalZerothCoefficientFactorizationAtAnchor : Prop

Local version of the classical factorization obligation at the rational elliptic anchor.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.localZerothCoefficientFactorizationAtAnchor_iff_global : LocalZerothCoefficientFactorizationAtAnchor ↔ GlobalZerothCoefficientFactorization

Analytic continuation turns factorization on the anchor patch into factorization on the full connected mass-zero collision-free phase domain.

theorem LeanPool.PoincareThreeBody.globalZerothCoefficientFactorization_iff_classicalPrinciple : GlobalZerothCoefficientFactorization ↔ ClassicalZerothCoefficientPrinciple

The canonical-section formulation is exactly equivalent to the energy-function formulation used by the normalization induction.

theorem LeanPool.PoincareThreeBody.nonintegrability_of_globalZerothCoefficientFactorization (hfactor : GlobalZerothCoefficientFactorization) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

With analytic mass division now proved, the exact challenge is reduced to the intrinsic classical factorization statement alone.