moon_J_cost_zero
plain-language theorem explainer
Moon's spin-orbit resonance ratio equals 1 and therefore carries zero J-cost under the Recognition Science cost function. Researchers modeling tidal locking in the inner Solar System cite this as the zero-cost base case that anchors all subsequent φ-ladder predictions. The proof is a one-line term reduction that substitutes the resonance definition and invokes the unit J-cost lemma.
Claim. Let $r=1$ be the Moon-Earth spin-orbit resonance ratio. Then the J-cost satisfies $J(r)=0$.
background
The Tidal Locking from φ-Resonance module treats spin-orbit resonances as points on the recognition lattice whose stability is quantified by the J-cost function. J-cost is defined by $J(x)=(x-1)^2/(2x)$, which is zero precisely at the trivial resonance $x=1$ and rises quadratically away from it. The Moon-Earth system is assigned the constant resonance parameter 1, corresponding to synchronous 1:1 rotation. This fact rests on the upstream lemma Jcost_unit0, which states that Jcost 1 = 0 by direct simplification of the cost definition.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of moon_resonance_pq (the constant 1) and then applies the lemma Jcost_unit0 from the Cost module, which directly yields Jcost 1 = 0.
why it matters
This theorem supplies the second clause of the TidalLockingFromPhiResonanceCert structure and is referenced inside the one-statement theorem tidal_locking_one_statement. It instantiates the T5 J-uniqueness property at the trivial fixed point, confirming that the 1:1 resonance is the absolute minimum of the cost function. The result closes the base case for the structural claim that every observed inner-Solar-System resonance lies within J(φ) of an integer or half-integer power of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.