Local energy leaves at the rational anchor

The interior elliptic action region contains a product box around the rational anchor in energy/first-action coordinates. Shrinking the first-action side to an interval ensures that the whole straight energy-leaf segment back to the anchor remains in the region.

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorFirstAction : ℝ

The first action used at the rational anchor.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorFirstAction = 1 / √3

theorem LeanPool.PoincareThreeBody.energyLeafAction_anchor : energyLeafAction (-2) delaunayAnchorFirstAction = delaunayAnchorAction

theorem LeanPool.PoincareThreeBody.analyticAt_energyLeafAction_parameters {energy firstAction : ℝ} (hfirstAction : firstAction ≠ 0) : AnalyticAt ℝ (fun (parameters : ℝ × ℝ) => energyLeafAction parameters.1 parameters.2) (energy, firstAction)

The straight energy-leaf action is jointly analytic in energy and first action away from L = 0.

theorem LeanPool.PoincareThreeBody.eventually_energyLeaf_segment_interior : ∀ᶠ (parameters : ℝ × ℝ) in nhds (-2, delaunayAnchorFirstAction), ∀ firstAction ∈ Set.uIcc parameters.2 delaunayAnchorFirstAction, energyLeafAction parameters.1 firstAction ∈ ProgradeEllipticActions ∧ firstAction ^ 2 * (1 + eccentricityFromActions (energyLeafAction parameters.1 firstAction)) < 1

Interior ellipticity holds throughout a whole short energy-leaf segment for every nearby energy/action pair.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.delaunayAnchorChart_eq_leadingActionCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {parameters : DelaunayAnchorParameters} (haction : parameters.1 ∈ ProgradeEllipticActions) (hapoapsis : parameters.1 0 ^ 2 * (1 + eccentricityFromActions parameters.1) < 1) : F 0 (delaunayAnchorChart parameters) = leadingActionCoefficient F parameters.1

On the interior part of the anchor chart, angle independence identifies the phase value with the action-section representative.

theorem LeanPool.PoincareThreeBody.hamiltonian_zero_delaunayAnchorChart {parameters : DelaunayAnchorParameters} (haction : parameters.1 ∈ ProgradeEllipticActions) : hamiltonian 0 (delaunayAnchorChart parameters) = delaunayHamiltonian parameters.1

The mass-zero Hamiltonian in the anchor chart is the Delaunay Hamiltonian of its action parameters.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.eventually_leadingActionCoefficient_eq_anchorEnergyCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) : ∀ᶠ (action : ActionSpace) in nhds delaunayAnchorAction, leadingActionCoefficient F action = leadingEnergyCoefficient F delaunayAnchorFirstAction (delaunayHamiltonian action)

Dense Poincaré resonances make every nearby leading action coefficient equal to the fixed anchor-section representative on the same energy leaf.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.eventually_globalEnergyCoefficient_eq_anchorEnergyCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) : ∀ᶠ (energy : ℝ) in nhds (-2), globalEnergyCoefficient F energy = leadingEnergyCoefficient F delaunayAnchorFirstAction energy

The canonical global energy section agrees locally with the fixed-anchor energy representative. Local openness supplies a nearby Delaunay preimage of every section point.

theorem LeanPool.PoincareThreeBody.localZerothCoefficientFactorizationAtAnchor_of_collisionBand : LocalZerothCoefficientFactorizationAtAnchor

The collision-band obstruction proves factorization on a genuine phase-space neighborhood of the rational anchor.

theorem LeanPool.PoincareThreeBody.globalZerothCoefficientFactorization_of_collisionBand : GlobalZerothCoefficientFactorization

The collision-band obstruction supplies the complete global zeroth-coefficient factorization.

theorem LeanPool.PoincareThreeBody.globalZerothCoefficientFactorization_of_densePoincareSet (_hdense : HasDenseClassicalPoincareSet) : GlobalZerothCoefficientFactorization

Backwards-compatible conditional form; the collision-band calculation now proves the factorization without assuming the full Poincaré set dense.

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

The proved collision-band calculation supplies the exact global nonintegrability theorem.

theorem LeanPool.PoincareThreeBody.nonintegrability_of_denseClassicalPoincareSet (_hdense : HasDenseClassicalPoincareSet) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

Conditional final form: the exact challenge follows from the sole remaining classical celestial-mechanics input, density of the Poincaré set.

theorem LeanPool.PoincareThreeBody.nonintegrability_of_analytic_separation (hseparation : HasAnalyticSeparatingResonantAverages) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

The exact challenge follows from the reduced analytic nonidentity form of Poincaré's disturbing-function calculation.

theorem LeanPool.PoincareThreeBody.nonintegrability_of_separation (hseparation : HasSeparatingResonantAverages) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

Final reduction after proving analyticity of the averaged disturbing function: it remains only to exhibit one separating eccentricity and two orientations at every positive resonance.