Separation of resonant disturbing averages in the collision band

The safe average stays finite at the boundary, while the aligned average tends to negative infinity. Hence the two orientation phases separate at an admissible eccentricity.

theorem LeanPool.PoincareThreeBody.exists_separating_resonantDisturbingAverages_of_collision_band {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) : ∃ (phaseA : ℝ) (phaseB : ℝ), ∃ witness ∈ admissibleResonantEccentricitySet p q, resonantDisturbingAverage p q witness phaseA - resonantDisturbingAverage p q witness phaseB ≠ 0

theorem LeanPool.PoincareThreeBody.dense_nondegenerateResonantEccentricities_of_collision_band {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) : Dense (nondegenerateResonantEccentricities p q)

For every rational resonance in the collision band, nondegenerate eccentricities are dense in the whole admissible fiber.