phiPow
plain-language theorem explainer
phiPow defines φ^n for each integer n as an element of ℤ[φ], supplying the φ-ladder that generates discrete scales in Recognition Science. Researchers constructing mass spectra or rung hierarchies cite it for explicit power construction. The definition uses direct cases for n=0 and n=1, a recursive Fibonacci-style builder for positive n via toNat conversion, and a zero placeholder for negatives.
Claim. For each integer $n$, define the power $φ^n$ as the element $a + bφ$ of $ℤ[φ]$ (with $a,b ∈ ℤ$) by the cases $φ^0 = 1$, $φ^1 = φ$, $φ^n = φ^{n-1} + φ^{n-2}$ for $n > 1$ (via iteration), and $φ^n = 0$ for $n < 0$.
background
PhiInt is the structure whose elements are pairs $(a,b)$ representing $a + bφ$ in the ring $ℤ[φ]$, equipped with the interpretation $a + bφ$ as a real number. The module Algebra.PhiRing develops the algebraic closure properties of φ under addition and multiplication, importing Cost and CostAlgebra for later physical interpretations. Upstream, toNat converts iteration counts from LogicNat to ℕ to drive the positive-power recursion, while the EightTick.prev supplies cyclic predecessor operations that align with the eight-tick octave.
proof idea
The definition matches on the sign of n. Zero and unit cases return the constants (1,0) and (0,1). For n > 1 it calls a local recursive build that starts from (φ^0, φ^1) and applies the recurrence (curr, curr + prev) exactly (n.toNat - 1) times, returning the second component. Negative n returns the zero placeholder.
why it matters
This definition realizes the φ-ladder, the fundamental scale structure of Recognition Science that enters the mass formula as yardstick · φ^(rung - 8 + gap(Z)). It directly encodes the self-similar fixed point of φ from the T0-T8 forcing chain and supplies the integer powers required for the eight-tick octave. Although no downstream uses appear yet, the construction closes the algebraic prerequisite for embedding the phi-ladder into cost and defect calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.