module module moderate

`IndisputableMonolith.Astrophysics.TidalLockingFromPhiResonance`

The module assembles definitions and equalities establishing the Moon-Earth 1:1 spin-orbit resonance as a phi-resonance outcome under J-cost minimization. Astrophysicists working on tidal evolution in the Recognition Science setting would cite these objects. The module is a collection of resonance predicates and cost statements built from the imported Constants and Cost primitives.

claimThe Moon-Earth system realizes a $1:1$ synchronous rotation expressed by the resonance predicate $p:q$ with associated $J$-cost zero at the phi-ladder rung fixed by the Recognition Composition Law.

background

The module resides in the Astrophysics domain and imports the RS-native time quantum $\tau_0 = 1$ tick from Constants together with the J-cost and defect machinery from Cost. It introduces sibling objects such as moon_resonance_pq (encoding the $p:q$ ratio), moon_resonance_eq, moon_J_cost_zero, and analogous statements for Mercury and Venus that measure deviations inside phi bands.

These objects apply the J-uniqueness relation $J(x) = (x + x^{-1})/2 - 1$ to spin-orbit couplings. The local theoretical setting is the extension of the eight-tick octave and phi self-similarity to orbital mechanics, with no additional physical constants introduced beyond the RS-native units.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete resonance predicates required for the phi-resonance account of tidal locking. It fills the astrophysical application step that follows T5 J-uniqueness and T7 octave structure, providing the Moon-Earth case that downstream solar-system analyses would invoke. No parent theorems are recorded in the used_by graph.

scope and limits

Does not derive the 1:1 ratio from orbital dynamics equations.
Does not contain numerical integration or simulation code.
Does not address non-synchronous resonances or exoplanet cases.
Does not prove stability of the resonance under perturbations.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

def moon_resonance_pq L87
def mercury_resonance_pq L90
def venus_resonance_pq L94
theorem moon_resonance_eq L99
theorem moon_J_cost_zero L102
theorem mercury_deviation_eq_J_phi L110
theorem mercury_deviation_in_J_phi_band L116
def phi_cubed L127
theorem phi_cubed_eq L130
theorem phi_cubed_band L141
theorem venus_deviation_in_inverse_phi_sq_band L149
def J_phi_ceiling L159
theorem J_phi_ceiling_pos L161
theorem J_phi_ceiling_band L165
structure TidalLockingFromPhiResonanceCert L189
def tidalLockingFromPhiResonanceCert L202
theorem tidal_locking_one_statement L226