toReal_sub
plain-language theorem explainer
Evaluation of the golden ring into the reals preserves subtraction: the image of a difference is the difference of the images. Anyone assembling the ring-homomorphism properties of the display map, or comparing discrete costs to classical J-cost, cites this. The proof rewrites subtraction as addition of a negative and applies the already-proved additive and negation lemmas.
Claim. For golden integers $x,y\in\mathbb{Z}[\varphi]$, the evaluation map $a+b\varphi\mapsto a+b\varphi_{\mathbb{R}}$ satisfies $\mathrm{ev}(x-y)=\mathrm{ev}(x)-\mathrm{ev}(y)$.
background
The module is the sigma1 display bridge from the golden ring $\mathbb{Z}[\varphi]$ into $\mathbb{R}$. Elements are pairs $(a,b)$ standing for $a+b\varphi$, with multiplication folded through the golden relation $\varphi^2=\varphi+1$. Evaluation sends $\langle a,b\rangle$ to $a+b\cdot\varphi_{\mathbb{R}}$, where $\varphi_{\mathbb{R}}$ is the classical positive root from PhiForcing.
All T6 forcing (uniqueness and positivity of the golden root) is already done at sigma0 inside $\mathbb{Z}[\varphi]$. This file only pays the continuum tax once, to show the discrete structure maps onto the classical presentation. Additive structure is already available: evaluation preserves addition and negation by direct expansion of coefficients.
Subtraction on golden integers is the ring difference $x+(-y)$. The present statement is the remaining additive-homomorphism clause needed before discrete costs can be compared to real $J$-cost.
proof idea
Rewrite the golden-integer difference via the ring identity $x-y=x+(-y)$. Apply the already-proved evaluation lemmas for addition and negation, which expand coefficient-wise into $\mathbb{R}$. Finish with a one-line ring normalization on the real side so the two expressions match. No continuum analysis beyond those two lemmas is required.
why it matters
This clause completes the additive half of the evaluation homomorphism used throughout the display bridge. Downstream, jdouble_eq_jcost rewrites $\mathrm{ev}(\mathrm{traceZ},n-2)$ by this lemma, equating the sigma0 doubled cost to $2\cdot J_{\mathrm{cost}}(\varphi^n)$ for the canonical cost $J(x)=(x+x^{-1})/2-1$. That identity is the T5 display bridge: the discrete Recognition Composition Law forced at sigma0 becomes the classical composition law on real $J$-cost.
In the forcing chain, T5 is $J$-uniqueness and T6 is $\varphi$ as the self-similar fixed point; both are derived discretely, and this homomorphism is pure display. It also parallels the subtraction transport on the recovered real line in RealsFromLogic, keeping the two evaluation stories aligned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.