toReal_phiInv
plain-language theorem explainer
The golden-integer inverse φ−1 evaluates under the real embedding to the classical reciprocal φ⁻¹. Anyone bridging the discrete golden ring ℤ[φ] to continuum φ-power statements cites this equality. The proof multiplies by φ inside ℤ[φ], pushes through the ring homomorphism, and invokes uniqueness of right inverses in ℝ.
Claim. Let $\mathbb{Z}[\varphi]$ be the golden ring of pairs $(a,b)$ representing $a+b\varphi$, and let $\mathrm{ev}:\mathbb{Z}[\varphi]\to\mathbb{R}$ send $(a,b)$ to $a+b\varphi$. Then $\mathrm{ev}(\varphi-1)=\varphi^{-1}$ in $\mathbb{R}$, where $\varphi-1$ is the exact multiplicative inverse of $\varphi$ inside $\mathbb{Z}[\varphi]$.
background
The module GoldenIntReal is the sigma1 display bridge from the discrete golden ring to the continuum. GoldenInt is the structure of pairs $(a,b)\in\mathbb{Z}^2$ representing $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. All of T6 (φ forced as the unique positive golden root) is derived inside this ring with only propext and Quot.sound.
The evaluation map toReal sends $\langle a,b\rangle$ to $a+b\cdot\varphi_{\mathbb{R}}$. It is a ring embedding: additive by construction, multiplicative because the integer product law matches real multiplication via PhiForcing.phi_equation, and injective by irrationality descent. Upstream, phiInv is defined exactly as $\langle -1,1\rangle$ (no division), and phi_mul_phiInv records $\varphi\cdot\varphi^{-1}=1$ by kernel computation.
The local point of the module is to pay Classical.choice once at the display boundary, so that sigma0 uniqueness and positivity theorems become statements about the real order rather than a private surrogate.
proof idea
Apply toReal_mul to the pair $(\varphi,\varphi^{-1})$ to obtain $\mathrm{ev}(\varphi\cdot\varphi^{-1})=\mathrm{ev}(\varphi)\cdot\mathrm{ev}(\varphi^{-1})$. Rewrite the left side with phi_mul_phiInv and toReal_one to get $1$, and the first factor on the right with toReal_phi to get $\varphi$. The resulting identity $\varphi\cdot\mathrm{ev}(\varphi^{-1})=1$ is then fed to eq_inv_of_mul_eq_one_right, which yields $\mathrm{ev}(\varphi^{-1})=\varphi^{-1}$.
why it matters
This lemma is the negative-exponent base case for toReal_phiZpow, which states that the unit-group power ladder in ℤ[φ] evaluates to ordinary real integer powers of φ. Without the inverse identity, the inductive step for negative integers cannot close.
In the Recognition forcing chain this sits at the T6 display boundary: φ is forced inside ℤ[φ] (sigma0 DELTA_FORCED), and the continuum presentation PhiForcing.φ is recovered only here. The reciprocal is the rung step that later feeds mass-ladder and eight-tick constructions, so matching discrete and classical inverses keeps the phi-ladder free of ad-hoc continuum constants.
The module doc frames the whole file as the single place where Real.sqrt and classical choice enter; this theorem is one of the concrete equalities that justify that tax.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.