phi_cubed_band
plain-language theorem explainer
The theorem establishes the strict numerical bounds 4.22 < phi cubed < 4.24. Researchers modeling inner Solar System spin-orbit resonances in the Recognition Science framework cite this interval to place Venus's 4:1 retrograde ratio near the cubic power on the phi-ladder. The proof is a term-mode reduction that substitutes the Fibonacci identity for phi cubed and closes both sides of the conjunction with linear arithmetic on the known bounds for phi.
Claim. $4.22 < phi^3 land phi^3 < 4.24$ where $phi$ is the golden ratio.
background
The Tidal Locking from phi-Resonance module interprets observed spin-orbit ratios as phi-rational minima of the J-cost on the phase manifold. Here phi denotes the golden ratio, the positive root of $x^2 - x - 1 = 0$, and phi cubed is defined as the cube of this value. Upstream results establish the identity phi cubed equals 2 phi plus 1 via the recurrence phi squared equals phi plus 1, together with the tight bounds 1.61 < phi and phi < 1.62. The module doc states that every observed resonance ratio lies within J(phi) of an integer or half-integer power of phi.
proof idea
The proof rewrites the target inequality via the phi cubed equality lemma, invokes the lower bound lemma phi greater than 1.61 and the upper bound lemma phi less than 1.62, then closes both conjuncts with linarith.
why it matters
This bound anchors the venus deviation theorem and populates the master TidalLockingFromPhiResonanceCert structure. It realizes the RS structural claim that the Venus 4:1 retrograde ratio sits near phi cubed, consistent with the phi-ladder and the self-similar fixed point. The result feeds the J phi ceiling band and aligns with the eight-tick octave and D equals 3 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.