phiZpow_add
plain-language theorem explainer
Integer powers of φ on the GoldenInt unit ladder multiply under addition of exponents: φ^(m+n)=φ^m·φ^n for all m,n∈ℤ. Anyone building the discrete d'Alembert identity for traceZ, or equating the unit-group ladder to real or ℕ ladders, cites this. The proof unfolds the unit-group definition and applies the standard integer power law.
Claim. For all integers $m,n$, writing $\varphi^k$ for the image in $\mathbb{Z}[\varphi]$ of the $k$-th power of the fundamental unit $\varphi$, one has $\varphi^{m+n}=\varphi^m\cdot\varphi^n$.
background
CostUniqueness re-derives T5 (J-cost uniqueness) on the discrete φ-ladder forced by T6, avoiding continuum choice. The carrier is GoldenInt = ℤ[φ]; negative powers are exact ring elements because φ⁻¹ = φ − 1 lies in the unit group.
phiZpow n is defined as the underlying GoldenInt of (phiUnit ^ n) in GoldenIntˣ. That makes φⁿ a pure ring element for every n∈ℤ, with no field inversion. The exponential law is the first algebraic identity needed before traces and the discrete RCL can be stated.
Upstream, the definition alone supplies the object; Mathlib's zpow_add on units supplies the multiplicative structure.
proof idea
One-line algebraic unwrap. Unfold phiZpow to expose the cast of a unit-group power, rewrite by Mathlib zpow_add (which gives (u^(m+n) = u^m * u^n) in the units), then rfl closes the equality after the cast to GoldenInt.
why it matters
This is the multiplicative skeleton of the φ-ladder inside the sigma0 T5 re-derivation. Downstream, traceZ_dAlembert expands both sides of the d'Alembert identity for traceZ n = φⁿ + φ⁻ⁿ by applying this law (and its negative-exponent twin) then ring. toReal_phiZpow uses the same step in the inductive bridge from GoldenInt to real powers of φ. phiPow_eq_phiZpow identifies the computable ℕ ladder with this unit-group ladder, so ladder-ratio bounds speak about the same carrier that hosts Jdouble and discrete RCL uniqueness.
In the framework, T5 on ℝ used continuity and Classical.choice; here the exponential law lets the whole uniqueness argument run by two-step induction on ℤ with no analytic residue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.