The classical obstruction for the leading coefficient

This file packages the density argument on the full prograde elliptic action region and pulls the resulting dependence back to physical phase space. The remaining celestial-mechanics input is isolated as ClassicalDisturbingNondegeneracy: the resonant disturbing average must be nonconstant at every rational resonance under consideration.

theorem LeanPool.PoincareThreeBody.not_linearIndependent_actionCovector_comp_of_wedge_eq_zero {u v : ActionSpace} (actionDerivative : PhaseSpace →L[ℝ] ActionSpace) (hwedge : wedge u v = 0) : ¬LinearIndependent ℝ ![actionCovector u ∘SL actionDerivative, actionCovector v ∘SL actionDerivative]

Pulling two dependent Euclidean action covectors back along any linear map cannot make them linearly independent.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (hnondegenerate : ClassicalDisturbingNondegeneracy) {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (hapoapsis : action 0 ^ 2 * (1 + eccentricityFromActions action) < 1) : wedge (delaunayFrequency (action 0)) (leadingActionDifferential F action) = 0

Poincaré's dense resonant set forces the leading candidate differential to be dependent on the Kepler frequency throughout the full interior prograde elliptic action region.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero_of_poincareSet {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (hdense : HasDenseClassicalPoincareSet) {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (hapoapsis : action 0 ^ 2 * (1 + eccentricityFromActions action) < 1) : wedge (delaunayFrequency (action 0)) (leadingActionDifferential F action) = 0

Natural classical form of the full action obstruction, assuming only density of the Poincaré set rather than nonvanishing at every rational resonance.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.mass_zero_differentials_dependent_on_liftedEllipse {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (hdense : HasDenseClassicalPoincareSet) {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; ¬LinearIndependent ℝ ![fderiv ℝ (hamiltonian 0) state, fderiv ℝ (F 0) state]

Physical form of the leading-coefficient obstruction on every noncircular lifted ellipse: the phase differentials of the zero-mass Hamiltonian and leading candidate are dependent.