phi_ninth_eq
plain-language theorem explainer
The identity states that the ninth power of the golden ratio satisfies phi to the ninth equals thirty four phi plus twenty one, continuing the Fibonacci recurrence pattern. Researchers deriving successive powers in the Recognition Science constants module would cite this step to advance the phi ladder. The proof is a short calc that multiplies the prior eighth power identity by phi and reduces via the quadratic relation.
Claim. $phi^9 = 34 phi + 21$, where $phi$ is the golden ratio obeying $phi^2 = phi + 1$.
background
The Constants module records numerical identities for the golden ratio phi that arise in Recognition Science derivations, with the fundamental time quantum set to one tick. The local setting treats phi as the self-similar fixed point whose powers obey the Fibonacci recurrence. Upstream lemmas supply the eighth power identity phi^8 equals twenty one phi plus thirteen and the quadratic phi^2 equals phi plus one; both are quoted directly in the calculation.
proof idea
A calc block begins with phi^9 equals phi times phi^8, substitutes the eighth power identity, applies ring to distribute, replaces phi squared by phi plus one using the quadratic lemma, and finishes with a final ring reduction to the target coefficients.
why it matters
The lemma feeds the tenth power identity in the same module, extending the chain of Fibonacci relations for phi powers. It supports the constants block that links to the forcing chain step where phi is fixed as the self-similar solution. The result closes one rung in the ladder used for mass and coupling derivations but leaves the general n case open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.