J_phi_ceiling_pos
plain-language theorem explainer
The theorem proves that the canonical golden-section J-cost ceiling is strictly positive. Researchers modeling spin-orbit resonances in the inner Solar System would cite it to bound the stability region around the golden ratio for Mercury's 3:2 lock. The proof is a one-line wrapper that unfolds the definition of the ceiling and invokes linear arithmetic on the known lower bound for phi.
Claim. $0 < phi - 3/2$, where $phi$ is the golden ratio.
background
In the Tidal Locking from φ-Resonance module, spin-orbit resonances are minima of the J-cost on the phase manifold. The ceiling is defined as J_phi_ceiling := phi - 3/2, the deviation bound |3/2 - phi| for Mercury's resonance ratio. This rests on the phi lower bound lemma from Constants, which shows phi > 1.61 via square-root inequalities on 2.22^2 < 5.
proof idea
The proof unfolds J_phi_ceiling := phi - 3/2 and applies the linarith tactic to the hypothesis phi > 1.61, which yields the strict inequality at once.
why it matters
This anchors the J-cost band for Mercury's resonance in the phi-ladder. It supports sibling claims such as mercury_deviation_in_J_phi_band by confirming the ceiling is positive, consistent with T5 J-uniqueness and the self-similar fixed point phi. It closes a structural step in the RS reading of observed spin-orbit ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.