toReal_add
plain-language theorem explainer
Additivity of the evaluation map from the golden integer ring ℤ[φ] into ℝ: ev(x+y)=ev(x)+ev(y). Cited by anyone using the ring embedding, the T6 display bridge, injectivity, or transported RCL/cosh identities. Proof unfolds componentwise addition and the evaluation formula, then closes by casting and ring arithmetic.
Claim. For all $x,y\in\mathbb{Z}[\varphi]$, writing $\mathrm{ev}(a+b\varphi)=a+b\,\varphi_{\mathbb{R}}$, one has $\mathrm{ev}(x+y)=\mathrm{ev}(x)+\mathrm{ev}(y)$.
background
The module is the sigma1 display bridge from the discrete golden ring into the continuum. GoldenInt is the structure of pairs $(a,b)\in\mathbb{Z}^2$ standing for $a+b\varphi$, with multiplication folded through $\varphi^2=\varphi+1$. All of T6 (forcing $\varphi$ as the unique positive golden root) is already proved inside that ring at sigma0; this file only evaluates into $\mathbb{R}$.
The evaluation map sends $\langle a,b\rangle$ to $a+b,\varphi_{\mathbb{R}}$, where $\varphi_{\mathbb{R}}$ is the classical positive root from PhiForcing. Addition on golden integers is componentwise: the $a$- and $b$-coordinates of $x+y$ are $x.a+y.a$ and $x.b+y.b$ (the simp lemmas used here). The continuum tax (Real.sqrt, classical choice) is paid exactly once at this boundary; the discrete derivation itself stays delta-forced.
proof idea
Three-step tactic proof. First simp only unfolds the evaluation definition and the two component lemmas for addition, rewriting both sides as integer casts plus $\varphi$-scaled casts. Then push_cast moves the $\mathbb{Z}\to\mathbb{R}$ coercions through the sums. Finally ring equates the two bilinear expressions in $\mathbb{R}$. No external lemmas beyond the local simp rules are required.
why it matters
This is the additive half of the claim that evaluation is a ring homomorphism $\mathbb{Z}[\varphi]\to\mathbb{R}$. Downstream it is used to prove injectivity (via $\mathrm{ev}(x-y)=0\Rightarrow x=y$), subtraction, and the trace identity $\mathrm{ev}(\mathrm{trace}_Z n)=\varphi^n+\varphi^{-n}$, which feeds the cosh display. It also appears in the T6 bridge (unique positive golden root evaluates to $(1+\sqrt{5})/2$) and in transporting the Recognition Composition Law and hyperbolic identities from recovered reals to Mathlib reals.
In the forcing chain this sits under T6: $\varphi$ is forced discretely, and additivity lets the discrete structure land on the classical presentation without re-proving uniqueness over $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.