phiPow_zero
plain-language theorem explainer
The computable φ-ladder evaluates to the unit of ℤ[φ] at rung zero: φ⁰ = 1. Anyone proving base cases for certified ladder ratios or bridging to the unit-group ladder cites this. The proof is pure definitional reflexivity from the structural recursion clause.
Claim. As an element of $\mathbb{Z}[\varphi]$, the structural power satisfies $\varphi^{0} = 1$.
background
The module LadderRatioBounds builds a sigma0-certified, kernel-reducible φ-ladder so that dimensionless mass ratios φᵏ become decidable integer statements. The local power phiPow : ℕ → GoldenInt is defined by structural recursion: the zero clause is the multiplicative unit 1 of ℤ[φ], and the successor multiplies by φ. Unlike the unit-group power phiZpow (which does not reduce under decide/#eval), this form prints and decides cleanly (e.g. phiPow 5 = ⟨3,5⟩).
Upstream, the Algebra.PhiRing ladder already records that φⁿ lies in ℤ[φ] for all integer n and obeys the Fibonacci recurrence. Here the ℕ-indexed version is re-introduced precisely so brackets such as RatLt/RatGt can close by decide inside {propext, Quot.sound} with no Real.sqrt or native_decide.
proof idea
One-line definitional reflexivity. The recursive equation sets the zero case to 1, so rfl discharges equality in GoldenInt. Marked @[simp] for automatic unfolding in later ladder identities.
why it matters
Base case for the bridge phiPow_eq_phiZpow, which states that the computable ladder agrees with the unit-group ladder of CostUniqueness on ℕ. That agreement lets every rational bracket proved here speak about the same φⁿ that carries traceZ/Jdouble at the T5 node. In the broader RS picture this is the n=0 anchor of the φ-ladder forced by T6: every mass-ratio gap is an integer power of the unique self-similar fixed point, and the zero power must be the dimensionless unit before any rung gap is applied. The module targets sigma0 DELTA_FORCED (Delta Forcing Spectrum program).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.