A phase avoiding every boundary collision

Shifting the aligned orientation by π/q puts it halfway between the possible collision phases. The exclusion is ultimately the parity contradiction 1 + 2ql = 2pk.

noncomputable def LeanPool.PoincareThreeBody.resonantSafeOrientation (p q : ℕ) : ℝ

An orientation halfway between resonant collision phases.

Equations

• LeanPool.PoincareThreeBody.resonantSafeOrientation p q = LeanPool.PoincareThreeBody.resonantCollisionOrientation p q + Real.pi / ↑q

theorem LeanPool.PoincareThreeBody.resonantCollisionEccentricity_apoapsis_identity {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : resonantSemimajorAxis p q * (1 + resonantCollisionEccentricity p q) = 1

theorem LeanPool.PoincareThreeBody.safeOrientation_primaryDistance_ne_zero_at_collisionBoundary {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) (time : ℝ) : (orientedResonantEllipsePosition p q (resonantCollisionEccentricity p q) (resonantSafeOrientation p q) time 0 - 1) ^ 2 + orientedResonantEllipsePosition p q (resonantCollisionEccentricity p q) (resonantSafeOrientation p q) time 1 ^ 2 ≠ 0

The safe orientation never meets the unit primary, even at the limiting collision eccentricity.