phiPow_five
plain-language theorem explainer
The fifth golden-ratio power equals 3 + 5φ inside ℤ[φ]. Anyone certifying dimensionless φ-ladder mass ratios or rung gaps at sigma0 cites this identity. Proof is a one-line kernel `decide` on the structural recursion for φ-powers.
Claim. In the ring $\mathbb{Z}[\varphi]$, one has $\varphi^5 = 3 + 5\varphi$, written as the coefficient pair $\langle 3, 5\rangle$.
background
Recognition Science places every spectral rung on the φ-ladder: two states separated by integer gap $k$ (same yardstick and gap class) stand in the exact dimensionless ratio $\varphi^k$. Here $\varphi$ is the T6 self-similar fixed point, and powers live in the golden integers $\mathbb{Z}[\varphi] = {a + b\varphi : a,b\in\mathbb{Z}}$.
This module computes those powers without the continuum. The local phiPow is defined by structural recursion: $\mathrm{phiPow},0 = 1$ and $\mathrm{phiPow}(n+1) = (\mathrm{phiPow},n)\cdot\varphi$. It reduces under both the Lean kernel and #eval, yielding Fibonacci coefficients $\langle F(n-1), F(n)\rangle$. Upstream PhiRing.phiPow is the same ladder idea over $\mathbb{Z}$, but the local version is the one that closes by decide at sigma0.
The surrounding program certifies rational brackets on $\varphi$ and on representative rungs ($\varphi^5$, the octave $\varphi^8$) via decidable sign predicates on $\mathbb{Z}[\varphi]$, all inside ${\mathrm{propext},\mathrm{Quot.sound}}$.
proof idea
One-line tactic proof: decide. Unfolding the recursive definition five times multiplies by $\varphi$ repeatedly in GoldenInt. Because multiplication and the base cases are definitional, the kernel reduces the left-hand side to the concrete pair $\langle 3, 5\rangle$ and closes equality by computation. No external lemmas are invoked.
why it matters
This is a kernel identity in the Delta Forcing Spectrum program (Delta_Forcing_Spectrum_20260626.tex): it makes the representative rung $\varphi^5$ an explicit, machine-checkable element of $\mathbb{Z}[\varphi]$. The mass law writes dimensionless ratios as yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$; certified powers are the arithmetic substrate for those ratios and for the rational brackets (RatLt/RatGt) proved later in the same module.
Framework landmarks: T6 forces $\varphi$ itself; T7’s eight-tick octave is the sibling identity $\varphi^8 = \langle 13, 21\rangle$ in the next theorem. The constant $Z_{\mathrm{cf}} = \varphi^5$ (Berry/creation threshold band) is exactly this rung. No downstream theorems currently depend on this declaration in the graph, but it is the computational witness the module’s certified brackets and #eval path rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.