phiZpow_one
plain-language theorem explainer
The unit-group ladder evaluates at exponent 1 to the golden-ratio generator itself inside ℤ[φ]. Discrete T5 / cost-uniqueness arguments cite this as the base rung of φⁿ before building the trace and J-double sequences. The proof is a three-step term reduction: unfold the unit power, apply the standard zpow identity at 1, and close by definitional equality.
Claim. On the golden-integer carrier, the integer power of the golden ratio at exponent one equals the generator: $\varphi^{1} = \varphi$.
background
CostUniqueness re-derives the T5 J-cost uniqueness node on the forced discrete carrier rather than on ℝ. The recognition ledger lives on the φ-ladder {φⁿ : n ∈ ℤ} forced by T6 self-similarity; there the Recognition Composition Law collapses to a two-step recurrence, so continuity and Classical.choice drop out.
The carrier is GoldenInt = ℤ[φ]. Powers are taken through the unit group: phiZpow n is the underlying ring element of (phiUnit)^n, so negative exponents are exact ring elements (φ⁻¹ = φ − 1) with no field division. The sibling exponential law states φ^(m+n) = φ^m · φ^n.
This base evaluation pins the n = 1 rung that later feeds the Chebyshev-style trace t(n) = φⁿ + φ⁻ⁿ and the discrete double-J sequence used for algebraic RCL uniqueness.
proof idea
Term-mode, three steps. Unfold the definition of the unit-group ladder so the goal is the underlying element of (phiUnit)^1. Rewrite by the standard integer-power identity zpow_one, which collapses any unit power at exponent 1 to the unit itself. Close by rfl against the definition of the golden-ratio generator inside GoldenInt.
why it matters
Base rung of the discrete φ-ladder that carries the sigma0 re-proof of T5. Downstream, traceZ_one rewrites the n = 1 trace through this identity (and the n = −1 sibling) to obtain t(1) = √5, the calibration value for d'Alembert uniqueness. GoldenIntReal.toReal_phiZpow uses it in the inductive step that the unit-group ladder matches real powers of φ. LadderRatioBounds.phiPow_eq_phiZpow cites it so computable ℕ-ladder brackets speak about the same φⁿ that carries traceZ and Jdouble.
In the framework this is the T6 carrier step under the T5 cost-uniqueness node: once φ¹ = φ is definitional, the discrete RCL and its unique normalized calibrated solution sit on exact ring arithmetic with no continuum pathology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.