`tidal_locking_one_statement`

proved

show as: view math explainer →

module: IndisputableMonolith.Astrophysics.TidalLockingFromPhiResonance
domain: Astrophysics
line: 226 · 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 226.

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

depends on

formal source

 223
 224All deviations sit at the canonical golden-section J-cost band,
 225forced by `Constants.phi` arithmetic. -/
 226theorem tidal_locking_one_statement :
 227    -- (1) Moon-Earth 1:1.
 228    moon_resonance_pq = 1 ∧
 229    -- (2) Moon at J-cost zero.
 230    Cost.Jcost moon_resonance_pq = 0 ∧
 231    -- (3) Mercury deviation in J(φ) band.
 232    (0.11 < phi - mercury_resonance_pq ∧
 233      phi - mercury_resonance_pq < 0.13) ∧
 234    -- (4) Venus deviation in 1/φ² band.
 235    (0.22 < phi_cubed - venus_resonance_pq ∧
 236      phi_cubed - venus_resonance_pq < 0.24) :=
 237  ⟨rfl,
 238   moon_J_cost_zero,
 239   mercury_deviation_in_J_phi_band,
 240   venus_deviation_in_inverse_phi_sq_band⟩
 241
 242end
 243
 244end TidalLockingFromPhiResonance
 245end Astrophysics
 246end IndisputableMonolith

papers checked against this theorem

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