venus_deviation_in_inverse_phi_sq_band
plain-language theorem explainer
The theorem establishes that the deviation of Venus's spin-orbit resonance ratio 4 from φ³ lies strictly between 0.22 and 0.24. Researchers modeling inner-Solar-System tidal locking via φ-resonance minima would cite it to locate the 4:1 retrograde case in the inverse-φ-squared band. The proof is a one-line wrapper that unfolds the constant definition of the resonance ratio and applies linear arithmetic to the established numerical band for φ³.
Claim. $0.22 < φ^3 - 4 < 0.24$, where φ denotes the golden ratio and 4 is the spin-orbit resonance ratio for the Venus-Sun 4:1 retrograde lock.
background
In the Recognition Science treatment of tidal locking, spin-orbit resonance ratios are φ-rational minima of the J-cost on the phase manifold. The golden ratio satisfies φ² = φ + 1, so φ³ = 2φ + 1. Venus's resonance ratio is the constant 4, corresponding to the observed slow retrograde rotation near a 4:1 lock. The upstream theorem phi_cubed_band supplies the numerical interval 4.22 < φ³ < 4.24. The module develops closed-form φ-ladder expressions for the three inner-Solar-System cases with zero axioms.
proof idea
The proof unfolds the definition of the Venus resonance ratio as the constant 4. It then invokes the theorem that places φ³ in (4.22, 4.24) and applies linear arithmetic to bound the positive difference in the target interval.
why it matters
The result is invoked by the one-statement theorem that collects the Moon 1:1 at J-cost zero, Mercury 3/2 within the J(φ) band of φ, and Venus 4 within the 1/φ² band of φ³. It completes the structural claim that every observed inner-Solar-System resonance ratio sits within J(φ) of an integer or half-integer power of φ, supporting the self-similar fixed point at φ in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.