phiPow_eight
plain-language theorem explainer
The eighth power of the golden ratio equals 13 + 21φ in ℤ[φ], the closed form of the octave rung on the φ-ladder. Anyone certifying ladder-ratio brackets, eight-tick structure, or J-cost at rung 8 cites this identity. Proof is a pure kernel decide on the Fibonacci recursion for φ-powers; no continuum or classical choice.
Claim. In the ring $\mathbb{Z}[\varphi]$, one has $\varphi^8 = 13 + 21\varphi$, where $\varphi$ is the golden ratio (T6 fixed point) and the right-hand side is the standard basis element $\langle 13, 21\rangle$.
background
Recognition Science places every mass rung on the φ-ladder: two states separated by integer gap $k$ stand in the exact dimensionless ratio $\varphi^k$. Here $\varphi$ is the unique self-similar fixed point forced at T6, and $\varphi^n$ lives in the order $\mathbb{Z}[\varphi]$.
This module builds a computable carrier phiPow : ℕ → GoldenInt by structural recursion (phiPow 0 = 1, phiPow (n+1) = phiPow n · φ). Unlike the unit-group ladder phiZpow, it reduces under both the kernel and #eval, and equals $\langle F(n-1), F(n)\rangle$ for the Fibonacci sequence $F$. The same module then certifies rational brackets on these powers via the sigma0 sign predicate on $\mathbb{Z}[\sqrt{5}]$.
Upstream, traceZ and Jdouble on the CostUniqueness ladder carry $t(n)=\varphi^n+\varphi^{-n}$ and $2J(\varphi^n)$; the module doc states that the computable ladder agrees with that unit-group ladder on ℕ, so the brackets speak about the same $\varphi^n$ that feeds the T5 J-node.
proof idea
One-line tactic proof: by decide. The recursive definition of the computable ladder unfolds eight multiplications by φ in ℤ[φ]. Equality of GoldenInt pairs is decidable, so the kernel reduces both sides to the normal form ⟨13, 21⟩ and closes the goal inside {propext, Quot.sound} with no classical choice and no native_decide.
why it matters
Rung 8 is the octave: T7 forces the eight-tick period $2^3$, and the mass formula measures rungs relative to the offset 8. Pinning $\varphi^8 = 13 + 21\varphi$ as a kernel fact supplies the exact algebraic value that rational brackets (RatLt/RatGt) and any later comparison of octave gaps rely on, all at sigma0 DELTA_FORCED.
It also aligns the computable ladder with the CostUniqueness carrier of traceZ/Jdouble (T5 J-uniqueness: $J(x)=(x+x^{-1})/2-1$). Downstream use is presently empty in the graph, but the sibling suite (phiPow_five, phi_lower, phi_upper, ratio witnesses) is built for the same certified-bracket pipeline in Delta_Forcing_Spectrum. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.