mercury_deviation_in_J_phi_band
plain-language theorem explainer
mercury_deviation_in_J_phi_band establishes that Mercury's 3:2 spin-orbit ratio deviates from φ by an amount strictly between 0.11 and 0.13. Researchers modeling tidal locking cite it to place the observed resonance inside the J(φ) stability band on the φ-ladder. The argument is a direct reduction to the resonance definition together with the bounding lemmas on φ.
Claim. $0.11 < φ - 3/2 ∧ φ - 3/2 < 0.13$
background
The module interprets inner-Solar-System spin-orbit resonances as J-cost minima on the φ-ladder, where J(x) = (x + x^{-1})/2 - 1 supplies the band ceiling J(φ) ≈ 0.118. Mercury's resonance is the constant ratio 3/2. The local setting is the RS claim that stable resonances sit within J(φ) of a φ-power, with the Moon at exact 1:1 (J-cost zero) and Venus near φ³.
proof idea
The proof is a term-mode wrapper. It unfolds the definition of the resonance ratio to 3/2, obtains the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo, and discharges both inequalities by linear arithmetic.
why it matters
The result supplies the Mercury clause of the master certificate TidalLockingFromPhiResonanceCert and the unified theorem tidal_locking_one_statement. It closes Track AS6 by confirming the 3:2 resonance lies inside the J(φ) band, consistent with J-uniqueness and the self-similar fixed point φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.