phiInv
plain-language theorem explainer
The multiplicative inverse of the golden ratio is realized inside the golden integers as the exact ring element −1 + φ (equivalently φ − 1). Anyone running the discrete T5 cost-uniqueness argument on the φ-ladder cites this carrier for negative powers. The body is a one-line structure constructor: no division, no field.
Claim. Define $\varphi^{-1}$ in the golden ring $\mathbb{Z}[\varphi]$ by the pair $(-1,1)$, i.e. the element $-1+\varphi$. Equivalently $\varphi^{-1}=\varphi-1$. This is an exact ring element, not a field quotient.
background
The module re-derives T5 cost-uniqueness on the discrete carrier forced by T6: the φ-ladder ${\varphi^n:n\in\mathbb{Z}}$ inside the golden ring. Over $\mathbb{R}$ the continuum proof of J-uniqueness needs continuity and classical choice to kill pathological solutions of the Recognition Composition Law; on the ladder the same law collapses to a two-step recurrence pinned by two initial values, so the argument is choice-free (sigma0).
GoldenInt is the structure of pairs $(a,b)$ standing for $a+b\varphi$, with multiplication folded through the minimal relation $\varphi^2=\varphi+1$. Units and integer powers of $\varphi$ are therefore ordinary ring elements: negative exponents never leave $\mathbb{Z}[\varphi]$.
The classical identity $\varphi^{-1}=\varphi-1$ is exactly the pair $(-1,1)$. That element is the seed for the unit-group powers used later to build $\mathrm{traceZ},n=\varphi^n+\varphi^{-n}$ and the discrete double-cost $G(n)=\mathrm{traceZ},n-2$.
proof idea
Pure definition: the structure constructor ⟨-1, 1⟩ of GoldenInt. No tactics, no lemmas. Downstream by decide theorems (phi * phiInv = 1, phiInv * phi = 1, phiInv = phi - 1) discharge the inverse and reciprocal identities by finite arithmetic in the ring.
why it matters
This is the exact inverse that lets negative ladder rungs stay inside $\mathbb{Z}[\varphi]$ without division. It feeds the unit package (phiUnit), the two-sided inverse laws, the reciprocal identity read from self-similarity, and phiZpow (including phiZpow_neg_one). Those powers build traceZ and the unique discrete solution of the d'Alembert form of RCL, which is the sigma0 re-proof of T5 J-uniqueness on the T6 carrier. The same carrier is reused by the algebraic PhiInt layer. Framework landmarks: T5 (J-cost uniqueness), T6 (φ as self-similar fixed point), RCL, and the choice-free delta-spine program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.