phiZpow_neg_mul
plain-language theorem explainer
On the GoldenInt carrier, every integer power of φ multiplies with its opposite power to 1: the φ-ladder rungs are units. Anyone building discrete T5 uniqueness or cancelling ladder factors cites this. The proof unfolds the unit-group definition of φⁿ and reduces via integer zpow additivity and cancellation.
Claim. For every $n \in \mathbb{Z}$, writing $\varphi^{k}$ for the image in $\mathbb{Z}[\varphi]$ of the $k$-th power of the fundamental unit, one has $\varphi^{-n}\cdot\varphi^{n}=1$.
background
CostUniqueness re-derives T5 (J-cost uniqueness) on the discrete φ-ladder forced by T6, rather than on ℝ. The carrier is GoldenInt = ℤ[φ], so negative powers need no field inversion: φ⁻¹ = φ − 1 is already a ring element, and powers run through the unit group GoldenIntˣ.
The map phiZpow sends n : ℤ to φⁿ as that unit's underlying GoldenInt value. Sibling facts already record the exponential law φ^{m+n} = φ^m · φ^n, the values at 0 and ±1, and φ · φ⁻¹ = 1. The present identity is the two-sided inverse law for arbitrary integer rungs.
Module goal: equip the ladder so that the discrete d'Alembert/trace sequence and the exact RCL for G(n) = 2J(φⁿ) can be stated and uniqueness-proved by induction, with no continuity and no Classical.choice.
proof idea
Short tactic proof. Unfold phiZpow to expose the coercion of (phiUnit ^ n) from GoldenIntˣ. Rewrite the product of values as the value of the product of units, then apply the integer power law zpow_add so the exponents become (−n) + n. Cancel to 0, reduce zpow_zero to the unit 1, and coerce Units.val_one back to the ring 1.
why it matters
Invertibility of every ladder rung is bookkeeping for the sigma0 T5 program: the Recognition Composition Law and the discrete cost G(n) = traceZ n − 2 live on {φⁿ : n ∈ ℤ}, so products and ratios of rungs must stay inside GoldenInt as exact units. This closes the negative-exponent half of the exponential calculus begun by phiZpow_add and the ±1 special cases.
Framework landmarks: T5 J-uniqueness (J(x) = (x + x⁻¹)/2 − 1) re-proved on the T6 self-similar carrier without continuum pathology; RCL is the target algebraic shape once traces are in place. No used_by edges are recorded yet; the natural consumers are the traceZ d'Alembert identities and the uniqueness induction for sequences satisfying the discrete composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.