phi_eighth_eq
plain-language theorem explainer
Golden ratio powers obey Fibonacci recurrences derived from the self-similar fixed point in Recognition Science. This lemma states the explicit algebraic form for the eighth power. Workers on frequency bands in photobiomodulation or octave scaling in economic models cite it directly. The proof is a short calc chain that multiplies by phi, substitutes the seventh-power identity, applies the quadratic relation, and collects terms.
Claim. $φ^8 = 21φ + 13$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The Constants module works in RS-native units with the fundamental time quantum set to one tick. Phi enters as the positive root of the quadratic $x^2 - x - 1 = 0$, forced as the self-similar fixed point (T6). Upstream lemmas supply the immediate predecessors: the seventh-power identity asserts $φ^7 = 13φ + 8$, while the square identity asserts $φ^2 = φ + 1$. These relations are built recursively from the defining equation of phi.
proof idea
The tactic proof is a calc block. It rewrites the left side as phi times phi to the seventh, substitutes the seventh-power identity, expands the product with ring, replaces the resulting phi squared term via the square identity, and finishes with a final ring simplification to the target coefficients.
why it matters
The identity feeds the ninth-power lemma and supplies the algebraic step for the gamma-band theorem that places $φ^8$ inside the 30-100 Hz EEG range. It also enters the octave-growth bound in ledger economics, a falsifiable prediction that $φ^8$ lies between 46 and 48. The result supports the eight-tick octave (T7) and the phi-ladder scaling used for mass and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.