TidalLockingFromPhiResonanceCert
plain-language theorem explainer
Recognition Science collects the master certificate for inner-planet tidal locking by bundling the exact resonance ratios of the Moon, Mercury and Venus with their measured deviations from powers of phi. A physicist working in the framework would cite the certificate when asserting that all three observed ratios sit inside the canonical J(phi) band of width approximately 0.12. The declaration is a pure record type whose eight fields are populated directly from the phi definition and the sibling band theorems.
Claim. Let $phi$ denote the golden ratio. The following eight relations hold: the Moon-Earth spin-orbit ratio equals 1 and its J-cost is exactly zero; the Mercury-Sun ratio equals $3/2$ with deviation $phi - 3/2$ strictly between 0.11 and 0.13; the Venus-Sun retrograde ratio equals 4; $phi^3 = 2phi + 1$ and $phi^3$ lies strictly between 4.22 and 4.24; the ceiling value $J(phi)$ lies strictly between 0.11 and 0.13.
background
In the Recognition Science reading of astrophysics, spin-orbit resonance ratios are the phi-rational minima of the J-cost on the phase manifold. The J-cost of a ratio r is obtained from the Recognition Composition Law as $J(r) = (r + r^{-1})/2 - 1$, with the canonical ceiling given by $J(phi) = phi - 3/2$. The module treats the Moon resonance as the trivial zero-cost point at ratio 1, the Mercury 3:2 resonance as the nearest half-integer to phi, and the Venus 4:1 retrograde resonance as the nearest integer to $phi^3$.
proof idea
The declaration is a structure definition that enumerates the eight required clauses with no proof obligations inside the structure itself. Each field is supplied by a direct reference to a sibling result: moon_resonance_eq by reflexivity on the constant 1, moon_J_cost_zero by the unit-cost lemma Cost.Jcost_unit0, mercury_deviation_in_J_phi_band by linarith on the phi bounds, and the phi-cubed identities and bands by the corresponding arithmetic theorems.
why it matters
The certificate supplies the complete arithmetic package needed to inhabit the downstream definition tidalLockingFromPhiResonanceCert, thereby closing Track AS6. It confirms that the observed resonances lie inside the J(phi) ceiling band predicted by the Recognition Composition Law and realizes the phi-ladder prediction for spin-orbit locking. The construction touches the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.