phi_cubed_eq
plain-language theorem explainer
Golden ratio satisfies the cubic identity φ³ = 2φ + 1. Astrophysicists and climate modelers cite this algebraic fact when deriving resonance bands or layer ratios inside phi-ladder constructions. The proof is a short calc chain that reduces the cube via the quadratic relation φ² = φ + 1 and applies ring normalization.
Claim. Let φ denote the golden ratio. Then φ³ = 2φ + 1.
background
The module supplies rigorous algebraic bounds on the golden ratio φ = (1 + √5)/2, starting from the quadratic relation φ² = φ + 1 and tightening decimal intervals such as 1.618 < φ < 1.6185. Upstream lemmas in Constants and the astrophysics and climate modules establish the same cubic identity as a direct consequence of that quadratic. The local setting is therefore purely algebraic verification inside the numerics interval package.
proof idea
The proof opens by invoking the quadratic goldenRatio_sq to obtain goldenRatio ^ 2 = goldenRatio + 1. It rewrites the cube as the square times goldenRatio, substitutes the quadratic, and reduces the resulting polynomial expression to 2*goldenRatio + 1 by three applications of ring.
why it matters
The identity supplies the exact algebraic reduction required by downstream certificates such as TidalLockingFromPhiResonanceCert and stratopause_tropopause_ratio_band. It fills the cubic step in the phi-ladder that Recognition Science uses to force self-similar fixed points and eight-tick octaves. The declaration is referenced in twenty dependent theorems across astrophysics and climate modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.