phi_cubed
plain-language theorem explainer
The golden ratio satisfies φ³ = 2φ + 1, equivalently F(3)φ + F(2) for the Fibonacci sequence. Astrophysicists and climate modelers cite the reduction when converting φ-powers into linear Fibonacci forms for resonance ratios and layering bounds. The proof is a one-line term reference to the established algebraic identity phi_cubed_eq from Constants.
Claim. $φ^3 = 2φ + 1$ (equivalently $F(3)φ + F(2)$ where $F$ is the Fibonacci sequence with $F(0)=0$, $F(1)=1$).
background
The Fibonacci-phi identity states that any power reduces via φ^n = F(n) φ + F(n-1). This supplies the arithmetic engine for per-domain bounds such as φ^8 > 46 in telomere models and φ^44 > 10^8 in baryon asymmetry calculations. The module CrossDomain.FibonacciPhiUniversality collects these identities as a zero-sorry cross-domain certificate, importing Constants and Mathlib.
proof idea
One-line term wrapper that applies the phi_cubed_eq lemma from IndisputableMonolith.Constants. That lemma expands by calc: phi^3 = phi * phi^2, substitutes phi^2 = phi + 1 from phi_sq_eq, then applies ring to reach 2*phi + 1.
why it matters
This supplies the cubic case of the universal identity, which feeds the TidalLockingFromPhiResonanceCert structure and the venus_deviation_in_inverse_phi_sq_band theorem for solar-system resonances. It completes the C20 cross-domain certificate step. In the Recognition framework it supports the phi-ladder reductions that derive D = 3 and mass formulas from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.