phiInv_eq_phi_sub_one

The module re-derives T5 cost-uniqueness on the forced discrete carrier of T6: the φ-ladder inside GoldenInt = ℤ[φ]. Continuum T5 needs continuity and classical choice to kill pathological RCL solutions on ℝ; on {φⁿ : n ∈ ℤ} the same law is a two-step recurrence pinned by two initial values, so the argument is pure algebra (sigma0).

Elements of ℤ[φ] are pairs ⟨a, b⟩ meaning a + b·φ. The golden ratio satisfies φ² = φ + 1, which rearranges multiplicatively to φ⁻¹ = φ − 1. The local definition packages that inverse as the concrete pair ⟨−1, 1⟩, an exact ring element rather than a quotient.

Negative ladder rungs are then ordinary multiplications by this unit, not divisions in a field. That is the carrier setup for phiZpow, traceZ, and the discrete RCL uniqueness argument that follows.

One-line computational proof: decide compares the defining pair of the inverse (⟨−1, 1⟩) with the pair for φ − 1 in the GoldenInt representation and closes by kernel equality. No algebraic lemmas are invoked beyond the decidable equality of coefficient pairs.

This identity is the multiplicative reading of T6 self-similarity (φ² = φ + 1) and is the reason negative exponents on the φ-ladder stay inside ℤ[φ] with no division. The module doc lists it as step 1 of the sigma0 T5 re-derivation: phiZpow n = φⁿ through the unit group, with φ⁻¹ = φ − 1 exact.

Downstream the same carrier builds traceZ n = φⁿ + φ⁻ⁿ (the discrete 2 cosh(n log φ)), proves the algebraic d'Alembert law, and obtains uniqueness of the discrete cost Jdouble under normalization and calibration. That closes the choice-free path from the Recognition Composition Law to J(x) = (x + x⁻¹)/2 − 1 on the ladder forced by T6, matching the continuum T5 node without continuity or Classical.choice.