The first Poincaré coefficient-normalization cycle #
The dense Poincaré-set obstruction makes the zeroth mass coefficient a local analytic function of the Kepler Hamiltonian. This file transfers that action-space statement to a physical lifted ellipse and instantiates the removable mass quotient. It is the complete local setup for one iteration of Poincaré's subtract-and-divide argument.
theorem
LeanPool.PoincareThreeBody.IsFirstIntegralFamily.mass_zero_eq_leadingEnergyCoefficient_hamiltonian
{δ : ℝ}
{F : ℝ → PhaseSpace → ℝ}
(hδ : 0 < δ)
(hanalytic : IsJointlyAnalytic δ F)
(hfirstIntegral : IsFirstIntegralFamily δ F)
(_hdense : HasDenseClassicalPoincareSet)
{firstAction eccentricity meanAnomaly periapsisAngle referenceFirstAction : ℝ}
(hfirstAction : 0 < firstAction)
(heccentricity : 0 < eccentricity)
(heccentricityOne : eccentricity < 1)
(hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1)
(hactionLeaf :
∀ candidateFirstAction ∈ Set.uIcc firstAction referenceFirstAction,
energyLeafAction (delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
candidateFirstAction ∈ ProgradeEllipticActions)
(hapoapsisLeaf :
∀ candidateFirstAction ∈ Set.uIcc firstAction referenceFirstAction,
candidateFirstAction ^ 2 * (1 + eccentricityFromActions
(energyLeafAction
(delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
candidateFirstAction)) < 1)
:
have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle;
F 0 state = leadingEnergyCoefficient F referenceFirstAction (hamiltonian 0 state)
On a connected local Kepler energy leaf, the mass-zero candidate is the analytic energy function constructed from any reference first action on that leaf.
theorem
LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_localLeadingEnergyCoefficient
{δ : ℝ}
{F : ℝ → PhaseSpace → ℝ}
(hδ : 0 < δ)
(hanalytic : IsJointlyAnalytic δ F)
{firstAction eccentricity meanAnomaly periapsisAngle referenceFirstAction : ℝ}
(hfirstAction : 0 < firstAction)
(heccentricity : 0 < eccentricity)
(heccentricityOne : eccentricity < 1)
(hactionReference :
energyLeafAction (delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
referenceFirstAction ∈ ProgradeEllipticActions)
(hapoapsisReference :
referenceFirstAction ^ 2 * (1 + eccentricityFromActions
(energyLeafAction (delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
referenceFirstAction)) < 1)
:
have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle;
AnalyticAt ℝ (leadingEnergyCoefficient F referenceFirstAction) (hamiltonian 0 state)
The local energy function used to cancel the zeroth coefficient is analytic at the physical Kepler energy of the lifted ellipse.
theorem
LeanPool.PoincareThreeBody.IsFirstIntegralFamily.analyticAt_massNormalizedCandidate_localEnergy_massSlice
{δ : ℝ}
{F : ℝ → PhaseSpace → ℝ}
(hδ : 0 < δ)
(hanalytic : IsJointlyAnalytic δ F)
(_hfirstIntegral : IsFirstIntegralFamily δ F)
(_hdense : HasDenseClassicalPoincareSet)
{firstAction eccentricity meanAnomaly periapsisAngle referenceFirstAction : ℝ}
(hfirstAction : 0 < firstAction)
(heccentricity : 0 < eccentricity)
(heccentricityOne : eccentricity < 1)
(hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1)
(hactionLeaf :
∀ candidateFirstAction ∈ Set.uIcc firstAction referenceFirstAction,
energyLeafAction (delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
candidateFirstAction ∈ ProgradeEllipticActions)
(hapoapsisLeaf :
∀ candidateFirstAction ∈ Set.uIcc firstAction referenceFirstAction,
candidateFirstAction ^ 2 * (1 + eccentricityFromActions
(energyLeafAction
(delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
candidateFirstAction)) < 1)
:
have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle;
AnalyticAt ℝ (fun (mass : ℝ) => massNormalizedCandidate F (leadingEnergyCoefficient F referenceFirstAction) mass state)
0
After cancelling the zeroth coefficient by the local analytic energy function, the mass-normalized candidate is analytic in mass at zero on the selected physical phase slice.
theorem
LeanPool.PoincareThreeBody.IsFirstIntegralFamily.mass_mul_massNormalizedCandidate_localEnergy
{δ : ℝ}
{F : ℝ → PhaseSpace → ℝ}
(hδ : 0 < δ)
(hanalytic : IsJointlyAnalytic δ F)
(hfirstIntegral : IsFirstIntegralFamily δ F)
(hdense : HasDenseClassicalPoincareSet)
{firstAction eccentricity meanAnomaly periapsisAngle referenceFirstAction mass : ℝ}
(hfirstAction : 0 < firstAction)
(heccentricity : 0 < eccentricity)
(heccentricityOne : eccentricity < 1)
(hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1)
(hactionLeaf :
∀ candidateFirstAction ∈ Set.uIcc firstAction referenceFirstAction,
energyLeafAction (delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
candidateFirstAction ∈ ProgradeEllipticActions)
(hapoapsisLeaf :
∀ candidateFirstAction ∈ Set.uIcc firstAction referenceFirstAction,
candidateFirstAction ^ 2 * (1 + eccentricityFromActions
(energyLeafAction
(delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity])
candidateFirstAction)) < 1)
:
have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle;
mass * massNormalizedCandidate F (leadingEnergyCoefficient F referenceFirstAction) mass state = normalizationResidual F (leadingEnergyCoefficient F referenceFirstAction) mass state
The same local normalization satisfies the exact subtract-and-divide identity at every mass on the chosen phase slice.