A concrete interior 1:2 resonance

This file specializes the finite-certificate interface to the 1:2 Kepler resonance at eccentricity 1 / 10. All geometric side conditions are proved exactly. A generated validated-numerics proof therefore only has to bound a second derivative and check one finite trapezoidal inequality.

noncomputable def LeanPool.PoincareThreeBody.oneTwoEccentricity : ℝ

The eccentricity selected for the concrete 1:2 resonance certificate.

Equations

• LeanPool.PoincareThreeBody.oneTwoEccentricity = 1 / 10

theorem LeanPool.PoincareThreeBody.resonantFirstAction_one_two_lt_four_fifths : resonantFirstAction 1 2 < 4 / 5

The 1:2 resonant first action is strictly less than the rational bound 4 / 5.

theorem LeanPool.PoincareThreeBody.oneTwoEccentricity_nonneg : 0 ≤ oneTwoEccentricity

The selected eccentricity is physically elliptic.

theorem LeanPool.PoincareThreeBody.oneTwoEccentricity_lt_one : oneTwoEccentricity < 1

theorem LeanPool.PoincareThreeBody.oneTwo_apoapsis_lt_one : resonantFirstAction 1 2 ^ 2 * (1 + oneTwoEccentricity) < 1

The selected ellipse lies strictly inside the orbit of the unit primary.

theorem LeanPool.PoincareThreeBody.oneTwo_exists_average_derivative_ne_zero_of_trapezoidal_certificate {phaseA phaseB errorBound : ℝ} {steps : ℕ} (hsecondDerivative : ∀ (time : ℝ), |iteratedDerivWithin 2 (resonantDisturbingDifference 1 2 oneTwoEccentricity phaseA phaseB) (Set.uIcc 0 (resonantOrbitPeriod 1)) time| ≤ errorBound) (hsteps : 0 < steps) (hcertificate : |resonantOrbitPeriod 1| ^ 3 * errorBound / (12 * ↑steps ^ 2) < |trapezoidal_integral (resonantDisturbingDifference 1 2 oneTwoEccentricity phaseA phaseB) steps 0 (resonantOrbitPeriod 1)|) : ∃ (orientation : ℝ), deriv (resonantDisturbingAverage 1 2 oneTwoEccentricity) orientation ≠ 0

A validated quadrature certificate for the selected phase pair gives a nonzero derivative of the exact resonant average, and hence the Poincaré homological obstruction on this orbit.