phiUnit
plain-language theorem explainer
Packages the golden ratio φ as a multiplicative unit of the ring ℤ[φ], with exact inverse φ⁻¹ = φ − 1. Anyone building the discrete φ-ladder (integer powers without division or field structure) cites this. The body is the standard unit-group constructor from the two kernel multiplication identities.
Claim. The golden ratio $\varphi$ is a unit of the ring $\mathbb{Z}[\varphi]$, with inverse $\varphi^{-1} = \varphi - 1$, witnessed by the identities $\varphi \cdot \varphi^{-1} = 1$ and $\varphi^{-1} \cdot \varphi = 1$.
background
The module re-derives T5 cost-uniqueness on the discrete carrier forced by T6: the φ-ladder ${\varphi^n : n \in \mathbb{Z}}$ inside $\mathrm{GoldenInt} = \mathbb{Z}[\varphi]$. Over $\mathbb{R}$, uniqueness of the J-cost under the Recognition Composition Law needs continuity and classical choice; on the ladder the same law collapses to a two-step recurrence pinned by two initial values, with no continuity axis.
Here $\varphi$ is the ring element $\langle 0,1\rangle$ (or the usual golden generator), and its inverse is defined exactly as $\varphi^{-1} = \varphi - 1 = \langle -1,1\rangle$, not by field division. The two theorems $\varphi \cdot \varphi^{-1} = 1$ and $\varphi^{-1} \cdot \varphi = 1$ are kernel computations (by decide). Packaging them yields a unit of $\mathrm{GoldenInt}^\times$, so integer powers stay inside the ring.
proof idea
Definitional constructor for the unit type: the four-tuple $(\varphi,,\varphi^{-1},,\varphi\cdot\varphi^{-1}=1,,\varphi^{-1}\cdot\varphi=1)$ is exactly the data of an element of $\mathrm{GoldenInt}^\times$. No tactic proof; the two multiplication lemmas are already discharged by decide.
why it matters
This is step 1 of the module's sigma0 program: expose $\varphi^n$ through the unit group so negative exponents are exact ring elements ($\varphi^{-1}=\varphi-1$), never fractions. The sole direct consumer is phiZpow, which defines $\varphi^n := (\mathrm{unit})^n$ as a $\mathrm{GoldenInt}$. That ladder then carries `traceZ n = \varphi^n + \varphi^{-n}$ (the discrete $2\cosh(n\log\varphi)$), the algebraic d'Alembert identity, and uniqueness of the discrete RCL solution calibrated at $\sqrt{5}-2$. In the forcing chain this closes the choice-free re-proof of T5 on the T6 carrier, replacing the continuum cosh-ODE argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.