phiPow_eq_phiZpow
plain-language theorem explainer
On natural numbers, the computable φ-ladder in ℤ[φ] equals the unit-group ladder φⁿ from CostUniqueness. Anyone citing sigma0 rational brackets on ladder rungs, or the real evaluation bridge, needs this identification. The proof is induction on n, using the Fibonacci recurrence on one side and the exponential law on the other.
Claim. For every natural number $n$, the structurally recursive power $\varphi^n \in \mathbb{Z}[\varphi]$ equals the image of the unit-group power $\varphi^n$ obtained by casting $n$ to $\mathbb{Z}$.
background
LadderRatioBounds builds a fully computable φ-ladder inside the golden integers ℤ[φ]: phiPow n is defined by structural recursion so that kernel decide and runtime #eval both reduce it (e.g. φ⁵ = ⟨3,5⟩). The point is certified rational brackets on rung ratios without Real, Float, or native_decide, staying inside sigma0 axioms.
Separately, CostUniqueness defines phiZpow n for n : ℤ by raising the unit φ to the n-th power in the unit group and forgetting units. That construction gives exact negative exponents and the exponential law φ^(m+n) = φ^m · φ^n, and it is the ladder that carries the T5 cost data (traceZ / Jdouble).
This theorem identifies the two ladders on ℕ. Upstream facts used are the base cases and recurrence for the computable ladder, together with phiZpow_zero, phiZpow_one, and phiZpow_add on the unit-group side.
proof idea
Induction on n.
Zero case: cast 0 : ℕ → ℤ is definitionally 0; rewrite with the zero lemmas on both ladders.
Successor case: cast (k+1) equals (k : ℤ) + 1 (omega). Rewrite the left side by the successor recurrence phiPow (k+1) = phiPow k · φ, apply the inductive hypothesis, then expand the right side by phiZpow_add and phiZpow_one so both sides become the same product.
why it matters
Without this equality, sigma0 brackets proved on the computable ladder would not automatically be statements about the same φⁿ that CostUniqueness uses for the T5 J-node and the forced self-similar ratio (T6). The sole direct consumer is toReal_phiPow in GoldenIntReal: it rewrites through this theorem, then through the real evaluation of phiZpow, to conclude that the computable ladder maps to classical real powers φ^n. That is the bridge from choice-free rational brackets (e.g. on φ, φ⁵, φ⁸) to genuine real inequalities on the RS mass-ladder ratios. In the Delta Forcing Spectrum program this keeps the dimensionless rung ratio end-to-end at sigma0 until the single Classical.choice step that lands in ℝ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.