J_phi_ceiling
plain-language theorem explainer
J_phi_ceiling defines the real number phi minus 3/2, serving as the numerical ceiling on J-cost deviations for phi-resonant spin-orbit ratios. Researchers modeling inner Solar System tidal locking cite it to bound the 3:2 Mercury resonance and similar cases within the Recognition Science lattice. The declaration is a single-line arithmetic definition with no proof obligations or auxiliary lemmas.
Claim. Let $phi$ denote the golden ratio. The J-cost ceiling is the real number $J_{phi ceiling} := phi - 3/2$.
background
The Tidal Locking from Phi Resonance module treats spin-orbit ratios as J-cost minima on the phase manifold, where J-cost follows the Recognition Composition Law. Phi is the self-similar fixed point from the forcing chain (T6), and resonances are required to lie within a band of width J(phi) around integer or half-integer powers of phi. The module doc states that Mercury's 3:2 ratio sits near phi with deviation approximately J(phi), while the Moon sits at exact zero cost and Venus near phi cubed.
proof idea
The declaration is a direct definition. It expands to the arithmetic subtraction phi - 3/2 with phi drawn from the imported Constants module; no tactics or lemmas are applied.
why it matters
This definition supplies the explicit ceiling value used by J_phi_ceiling_band, J_phi_ceiling_pos, and the TidalLockingFromPhiResonanceCert structure to certify that Mercury's deviation lies in (0.11, 0.13). It anchors the phi-resonance band to the T6 fixed point and the eight-tick octave in the RS framework, closing the structural claim for inner Solar System resonances with zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.