venus_resonance_pq
plain-language theorem explainer
Venus resonance ratio is the constant 4 that encodes the observed 4:1 spin-orbit lock for Venus-Sun in slow retrograde rotation. Modelers of inner-solar-system tidal evolution cite this integer when testing whether observed ratios sit inside J-cost bands on the φ-ladder. The declaration is a direct real-number assignment with no reduction steps.
Claim. The Venus-Sun spin-orbit resonance ratio is the real number $4$.
background
Recognition Science treats spin-orbit resonances as J-cost minima on the phase manifold, where J(x) = (x + x^{-1})/2 - 1. The φ-ladder supplies reference ratios: φ for Mercury's 3:2 and φ³ ≈ 4.236 for Venus's retrograde 4:1. The cost function is the derived comparator cost from the multiplicative recognizer, non-negative by construction. This module supplies the integer p/q values that feed the deviation-band theorems for the inner solar system.
proof idea
One-line definition that directly assigns the integer 4 to the Venus resonance ratio.
why it matters
The definition supplies the Venus integer to TidalLockingFromPhiResonanceCert and the one-statement theorem tidal_locking_one_statement. It completes the structural claim that all three inner-solar resonances lie at φ-rational positions, linking to T5 J-uniqueness and the φ-ladder. The downstream deviation theorem then verifies that |4 - φ³| lies inside the inverse-φ² band (0.22, 0.24).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.