toReal_neg
plain-language theorem explainer
The evaluation map from golden integers ℤ[φ] into ℝ sends additive inverses to additive inverses. Anyone assembling the ring-homomorphism properties of the display bridge cites this identity. The argument unfolds coordinate-wise negation and the linear evaluation formula, then closes by ordinary ring arithmetic after integer-to-real casting.
Claim. For every golden integer $x=a+b\varphi$ with $a,b\in\mathbb{Z}$, the real evaluation satisfies $\mathrm{ev}(-x)=-\mathrm{ev}(x)$, where $\mathrm{ev}(a+b\varphi)=a+b\,\varphi_{\mathbb{R}}$ and $\varphi_{\mathbb{R}}$ is the classical positive golden root.
background
Golden integers are pairs $(a,b)\in\mathbb{Z}^2$ standing for $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. Negation is componentwise: $(-x)$ has coordinates $(-a,-b)$. The evaluation map of this module sends $\langle a,b\rangle$ to the real $a+b,\varphi_{\mathbb{R}}$, where $\varphi_{\mathbb{R}}$ is the classical golden ratio from PhiForcing.
This file is the sigma1 display boundary: the sigma0 derivation of T6 (φ forced as the unique positive golden root) lives entirely inside ℤ[φ]; here one pays the continuum tax once by embedding into ℝ and matching the classical presentation. Upstream, phi_equation records $\varphi^2=\varphi+1$ on both the algebraic and real sides, and the simp lemmas for the negated coordinates are definitional.
proof idea
Unfold the evaluation definition together with the two coordinate lemmas for negation. After push_cast moves the integer negations into ℝ, the goal is the elementary identity $-(a+b\varphi_{\mathbb{R}})=(-a)+(-b)\varphi_{\mathbb{R}}$, which ring discharges. No appeal to $\varphi^2=\varphi+1$ is required; additivity of the linear form is enough.
why it matters
Additive inversion is one of the ring-homomorphism clauses for the display map. Downstream it is used to build subtraction (toReal_sub), injectivity of evaluation (via $x+(-y)$ and the kernel criterion), and the sign bridge that equates the decidable sigma0 predicate IsPos with ordinary real positivity. Rational comparison lemmas such as ratGt_toReal rewrite through this identity when a witness difference is negated. Farther out, the LogicReal transcendental layer reuses the same pattern when transporting cosh identities. In the Recognition chain this sits inside the T6 display bridge: uniqueness and positivity of φ are proved at sigma0; only the continuum readout needs these homomorphism facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.