phi_cubed_eq
plain-language theorem explainer
The identity phi cubed equals two phi plus one follows from the golden ratio quadratic. Researchers deriving spin-orbit resonances for Venus cite it to anchor the 4:1 ratio near phi cubed on the recognition ladder. The tactic proof unfolds the definition, substitutes the square relation twice, and closes with ring normalization.
Claim. Let $phi$ be the positive root of $x^2 - x - 1 = 0$. Then $phi^3 = 2 phi + 1$.
background
The module treats spin-orbit resonance ratios as phi-rational minima of J-cost on the phase manifold. phi_cubed is defined as phi raised to the third power, placing the Venus retrograde ratio of 4 near this value with deviation 1 over phi squared. The local setting is a structural theorem for inner Solar System resonances with zero sorrys: Moon at 1:1 with J-cost zero, Mercury at 3/2 near phi, Venus at 4 near phi cubed.
proof idea
Tactic-mode proof. Unfold phi_cubed, obtain h from phi_sq_eq that phi squared equals phi plus one, introduce h_step that phi cubed equals phi squared times phi by ring, rewrite the step and h, apply ring_nf, rewrite h again, and finish with ring.
why it matters
This identity feeds the master certificate TidalLockingFromPhiResonanceCert and the band theorem phi_cubed_band that verifies the numerical interval. It is reused in the Climate module for stratopause to tropopause ratio. In the Recognition framework it instantiates the self-similar fixed point phi (T6) and supports the structural claim that observed resonances lie within J(phi) of integer or half-integer powers of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.