phiZpow_zero
plain-language theorem explainer
On the GoldenInt carrier, the unit-group ladder satisfies φ⁰ = 1. Downstream base cases for the discrete trace, the real embedding of the ladder, and the computable-vs-unit ladder agreement all cite this identity. The proof unfolds the unit-group definition and applies the standard integer power law zpow_zero.
Claim. Writing $\varphi^n$ for the image of the unit-group power of the golden-ratio unit in $\mathbb{Z}[\varphi]$, one has $\varphi^0 = 1$.
background
The module CostUniqueness re-derives the T5 cost-uniqueness node on the discrete φ-ladder forced by T6, working entirely inside GoldenInt = ℤ[φ] so that negative powers are exact ring elements (φ⁻¹ = φ − 1) with no field division and no Classical.choice.
The ladder is defined by phiZpow n = ((phiUnit ^ n : GoldenIntˣ) : GoldenInt), i.e. integer powers of the golden unit through the unit group. The exponential law φ^(m+n) = φ^m · φ^n is the companion identity. The zero case is the normalization that every subsequent discrete identity (trace, d'Alembert recurrence, discrete RCL) needs at n = 0.
Upstream, only the definition of this ladder is required; the ambient Mathlib fact is that any group power satisfies g⁰ = 1.
proof idea
Term-mode unfold of the ladder definition reduces the claim to the unit-group power (phiUnit ^ 0 : GoldenIntˣ) casting to GoldenInt. Rewrite with Mathlib zpow_zero yields the unit 1 of GoldenIntˣ, and rfl closes after the coercion.
why it matters
This is the n = 0 anchor of the discrete φ-ladder that carries the choice-free T5 argument. It is used by traceZ_zero to obtain traceZ 0 = 2 (the d'Alembert normalization h(0) = 2), by toReal_phiZpow as the base of the induction equating the unit-group ladder to real powers of φ, and by phiPow_eq_phiZpow as the base equating the computable ℕ-ladder to the same carrier that supports traceZ and Jdouble.
In the framework, T5 forces J(x) = (x + x⁻¹)/2 − 1 via the Recognition Composition Law; on the φ-ladder the continuum ODE step collapses to a two-step recurrence, and this identity is the first pin of that recurrence. Without φ⁰ = 1 the discrete normalization G(0) = 0 for Jdouble cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.