tidal_locking_one_statement
plain-language theorem explainer
The theorem collects the inner-Solar-System spin-orbit ratios into one assertion: Moon-Earth at exactly 1 with J-cost zero, Mercury 3:2 within (0.11, 0.13) of phi, and Venus 4 within (0.22, 0.24) of phi cubed. Celestial mechanicians and recognition-physics modelers would cite it as a structural check that observed resonances sit at golden-section J-cost minima. The proof is a term-mode tuple that directly assembles reflexivity for the equality together with the three prior band and zero-cost lemmas.
Claim. Let $r_M=1$, $r_{Hg}=3/2$, $r_V=4$, and let $J$ be the J-cost function. Then $r_M=1$, $J(r_M)=0$, $0.11<phi-r_{Hg}<0.13$, and $0.22<phi^3-r_V<0.24$.
background
In this module the J-cost is the Recognition Science cost function that vanishes at integer ratios and rises with deviation from phi-rational points on the lattice. The sibling definitions fix moon_resonance_pq as the Moon-Earth ratio 1, mercury_resonance_pq as the Mercury-Sun 3:2 ratio, venus_resonance_pq as the Venus-Sun 4 ratio, and phi_cubed as phi raised to the third power. Upstream lemmas already establish that Jcost(1)=0 via the unit-cost axiom and that the two deviation intervals lie inside the canonical J(phi) and 1/phi squared bands.
proof idea
The proof is a one-line term-mode wrapper that supplies the four conjuncts of the conjunction: reflexivity for the equality moon_resonance_pq=1, the zero-cost theorem moon_J_cost_zero, the Mercury band theorem mercury_deviation_in_J_phi_band, and the Venus band theorem venus_deviation_in_inverse_phi_sq_band.
why it matters
This declaration closes Track AS6 by packaging the three canonical inner-Solar-System resonances into a single proved statement. It sits immediately downstream of the individual resonance definitions and deviation-band lemmas, and it instantiates the phi-ladder and J-cost ceiling that arise from the forcing chain (T5 J-uniqueness and T6 phi fixed point). No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.