`moon_resonance_pq`

definition

show as: view math explainer →

module: IndisputableMonolith.Astrophysics.TidalLockingFromPhiResonance
domain: Astrophysics
line: 87 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Astrophysics.TidalLockingFromPhiResonance on GitHub at line 87.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  84/-! ## §1. Resonance ratios for canonical Solar-System bodies -/
  85
  86/-- Moon-Earth spin-orbit ratio: 1:1 synchronous rotation. -/
  87def moon_resonance_pq : ℝ := 1
  88
  89/-- Mercury-Sun spin-orbit ratio: 3:2 (3 rotations per 2 orbits). -/
  90def mercury_resonance_pq : ℝ := 3 / 2
  91
  92/-- Venus-Sun spin-orbit ratio: 4:1 (slow retrograde, period
  93ratio ≈ 4). -/
  94def venus_resonance_pq : ℝ := 4
  95
  96/-! ## §2. Moon: trivial 1:1 resonance at J-cost zero -/
  97
  98/-- Moon-Earth ratio is exactly 1. -/
  99theorem moon_resonance_eq : moon_resonance_pq = 1 := rfl
 100
 101/-- Moon sits at J-cost zero (trivial resonance). -/
 102theorem moon_J_cost_zero : Cost.Jcost moon_resonance_pq = 0 := by
 103  unfold moon_resonance_pq
 104  exact Cost.Jcost_unit0
 105
 106/-! ## §3. Mercury: 3/2 sits near φ -/
 107
 108/-- Mercury's `p/q = 3/2` is near `φ ≈ 1.618`; the deviation is
 109`|φ - 3/2| = J(φ) ≈ 0.118`. -/
 110theorem mercury_deviation_eq_J_phi :
 111    phi - mercury_resonance_pq = phi - 3 / 2 := by
 112  unfold mercury_resonance_pq
 113  ring
 114
 115/-- The deviation `|φ - 3/2|` is positive and below `J(φ)`-band ceiling. -/
 116theorem mercury_deviation_in_J_phi_band :
 117    0.11 < phi - mercury_resonance_pq ∧

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.