phiPow
plain-language theorem explainer
Natural-number powers of the golden ratio as explicit elements of the golden integer ring Z[φ], built by structural recursion so they reduce under decide and #eval. Anyone certifying rational brackets on ladder rungs (φ⁵, φ⁸, the octave) cites this carrier. The body is the recursive product with base case 1; no lemmas are needed.
Claim. For each natural number $n$, $\varphi^n$ is the element of $\mathbb{Z}[\varphi]$ given by $n$-fold multiplication by $\varphi$: $\varphi^0 = 1$ and $\varphi^{n+1} = \varphi^n \cdot \varphi$.
background
LadderRatioBounds certifies forced φ-ladder ratios with rational brackets at sigma0 (choice-free integer arithmetic on Z[φ]). In Recognition Science every mass-spectrum rung sits on the φ-ladder: states separated by integer gap k stand in the exact dimensionless ratio φ^k. φ itself is the T6 self-similar fixed point; the mass law is yardstick times a φ-power.
GoldenInt is the golden ring Z[φ]: pairs (a, b) for a + b·φ, with multiplication folded through φ² = φ + 1. Upstream, PhiRing.phiPow supplies the full integer ladder ("the fundamental scale structure of RS") with the key property that φⁿ lies in Z[φ] for all n ∈ Z. The present definition restricts the domain to ℕ and uses structural recursion so the kernel and compiler reduce it cleanly: the n-th power equals ⟨F(n−1), F(n)⟩ for Fibonacci F, unlike the unit-group route which does not reduce under decide or #eval.
proof idea
Definition by structural recursion on ℕ. Base case sends 0 to the multiplicative unit 1 of GoldenInt. The successor clause multiplies the previous power by the ring element φ. No lemmas fire; the body is exactly that recursive equation. The form is chosen so decide and #eval reduce concrete powers (e.g. the fifth power prints as ⟨3, 5⟩).
why it matters
Computable carrier for the forced dimensionless ladder ratios in the Delta Forcing Spectrum program (sigma0 DELTA_FORCED). Downstream, ladder_ratio_brackets pins φ, φ⁵, and φ⁸ inside explicit rational intervals entirely by decide on the RatLt/RatGt predicates; the concrete theorems phi5_lower, phi5_upper, phi8_lower, and phi8_upper apply this definition directly. GoldenIntReal.toReal_phiPow evaluates the ℕ-ladder to classical real powers of φ, and ratGt_toReal lifts the sigma0 brackets to genuine real inequalities.
Framework landmarks: T6 forces φ; T7 is the eight-tick octave (period 2³), whose representative rung is φ⁸; Z_cf = φ⁵ lies in (11, 12) and appears in the Berry/creation threshold story. The real-side reading of the whole bracket bundle is GoldenIntReal.ladder_ratio_real_brackets (sigma1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.