phi_mul_phiInv
plain-language theorem explainer
In the golden-integer ring ℤ[φ], the product of φ with its exact inverse φ−1 equals the multiplicative identity. Anyone assembling the unit group for the discrete φ-ladder cites this identity. The proof is a one-line kernel decision on the integer-pair representation.
Claim. In the ring $\mathbb{Z}[\varphi]$, writing $\varphi^{-1}:=\varphi-1$, one has $\varphi\cdot\varphi^{-1}=1$.
background
The CostUniqueness module re-derives the T5 cost-uniqueness node on the discrete carrier forced by T6: the φ-ladder ${\varphi^n:n\in\mathbb{Z}}$ inside GoldenInt $=\mathbb{Z}[\varphi]$. Elements are pairs $\langle a,b\rangle$ meaning $a+b\varphi$, so ring arithmetic is exact and choice-free (sigma0).
The inverse is not obtained by field division. It is the ring element $\varphi^{-1}=\varphi-1=\langle-1,1\rangle$, which is already in $\mathbb{Z}[\varphi]$. This identity is the first half of the unit-group data needed to form integer powers $\varphi^n$ for negative $n$ without leaving the ring.
Upstream, the sibling definition supplies that inverse element; the module goal is to pin the discrete Recognition Composition Law solution $J(\varphi^n)$ by a two-step recurrence rather than by continuum ODE uniqueness.
proof idea
Term-mode proof by decide. On the pair representation, multiplication of $\langle 0,1\rangle$ by $\langle-1,1\rangle$ expands to the integer coefficients of $1=\langle 1,0\rangle$ by the golden-ratio minimal polynomial $\varphi^2=\varphi+1$. No lemmas are invoked beyond the decidable equality of GoldenInt.
why it matters
This is the left-inverse half of the unit constructor that packages φ as an element of GoldenIntˣ. Downstream, that unit feeds the integer power ladder φⁿ (negative exponents stay exact ring elements) and the real-embedding lemma that evaluates the sigma0 inverse to the ordinary real φ⁻¹.
In the Recognition forcing chain this sits under T5/T6: once φ is the self-similar fixed point, the ladder must be a group under multiplication, and the cost J on that ladder is then unique by algebraic induction rather than by Classical.choice continuum arguments. The companion right-inverse identity is the symmetric sibling; together they close the unit data used throughout DeltaSpine and the PhiRing algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.