tidalLockingFromPhiResonanceCert
plain-language theorem explainer
The master certificate TidalLockingFromPhiResonanceCert assembles eight clauses confirming that the Moon-Earth, Mercury-Sun, and Venus-Sun spin-orbit ratios lie at φ-rational positions with J-cost deviations bounded by the golden-section band. Astrophysicists modeling tidal evolution would cite it to replace numerical happenstance with Recognition Science arithmetic. The proof is a one-line wrapper that populates the structure fields by reflexivity for exact equalities and direct references to prior lemmas for the numerical bands.
Claim. Let $p/q$ denote the spin-orbit resonance ratio and $J$ the J-cost function. Then the Moon-Earth ratio satisfies $p/q=1$ with $J(p/q)=0$, the Mercury-Sun ratio satisfies $p/q=3/2$ with $0.11<φ-3/2<0.13$, the Venus-Sun ratio satisfies $p/q=4$ with $φ^3∈(4.22,4.24)$, and $φ^3=2φ+1$, where $φ$ is the golden ratio.
background
The module treats spin-orbit resonance ratios as φ-rational minima of the J-cost on the phase manifold. The structure TidalLockingFromPhiResonanceCert packages eight clauses: moon_resonance_pq=1, Cost.Jcost moon_resonance_pq=0, mercury_resonance_pq=3/2, the deviation |φ-3/2| inside (0.11,0.13), venus_resonance_pq=4, phi_cubed=2φ+1, and phi_cubed inside (4.22,4.24). Upstream lemmas supply the exact equalities (moon_resonance_eq, mercury_resonance_eq) and the band theorems (J_phi_ceiling_band, mercury_deviation_in_J_phi_band, phi_cubed_band). Constants.phi supplies the real-arithmetic value of the golden ratio used throughout.
proof idea
The definition constructs the structure by field assignment. Exact equalities receive rfl. The J-cost zero clause and the three numerical-band clauses receive direct references to the supporting theorems moon_J_cost_zero, mercury_deviation_in_J_phi_band, phi_cubed_band, J_phi_ceiling_band, and phi_cubed_eq.
why it matters
This definition inhabits the master certificate for Track AS6, closing the structural theorem that the observed inner-Solar-System resonances sit at φ-rational positions forced by Constants.phi arithmetic. It supplies the eight clauses referenced in the one-statement summary at the foot of the module. The result sits inside the Recognition Science forcing chain at the level of J-uniqueness and the self-similar fixed point φ, replacing conventional tidal-evolution numerics with lattice minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.