toReal_one
plain-language theorem explainer
The multiplicative unit of the golden integers evaluates to the real number 1 under the display map a+bφ ↦ a+b·φ_ℝ. Anyone normalizing ring-homomorphism identities, inverse relations, or integer powers on the φ-ladder will cite this simp lemma. The proof is a one-line unfolding of the evaluation definition.
Claim. The evaluation map $\mathbb{Z}[\varphi]\to\mathbb{R}$ given by $a+b\varphi\mapsto a+b\varphi_{\mathbb{R}}$ sends the multiplicative unit $1$ to $1\in\mathbb{R}$.
background
The module GoldenIntReal is the sigma1 display bridge from the discrete ring $\mathbb{Z}[\varphi]$ (built in GoldenInt with only propext and Quot.sound) into classical $\mathbb{R}$. The derivation of T6 (φ forced as the unique positive golden root) stays inside $\mathbb{Z}[\varphi]$; this file pays the continuum cost once by evaluating into Mathlib reals.
The evaluation map is defined by $\mathrm{toReal}(\langle a,b\rangle)=a+b\cdot\varphi$, where $\varphi$ is the classical golden ratio from PhiForcing. Sibling lemmas establish that this map is a ring embedding (additivity, multiplicativity via $\varphi^2=\varphi+1$, injectivity via irrationality descent) and that the discrete positivity predicate matches real positivity.
This unit lemma is the base case for that ring-homomorphism package: the multiplicative identity must land on $1$ before products, inverses, and $\mathbb{Z}$-powers can be transported.
proof idea
One-line simp proof. Unfold the definition of the evaluation map on the golden-integer unit (coefficients $a=1$, $b=0$), so the real expression collapses to $1+0\cdot\varphi=1$. No external lemmas beyond the definition are required.
why it matters
This is the unit clause of the display bridge that lets sigma0 T6 results speak classical language. Downstream, t6_bridge uses the package to identify the discrete positive golden root with $(1+\sqrt{5})/2$; toReal_phiInv rewrites $\varphi\cdot\varphi^{-1}=1$ after evaluation and needs the unit identity on the right-hand side; toReal_phiZpow takes the zero-power case of the unit-group ladder by reducing to this lemma and $zpow_zero$.
In the broader forcing chain, T6 forces φ as the self-similar fixed point inside $\mathbb{Z}[\varphi]$. The display layer (this module) only translates that uniqueness into the continuum presentation used by PhiForcing and recovered constants such as phiL_gt_one. Without the unit identity, none of the multiplicative transport steps close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.