toReal_zero

This module is the display bridge from the golden integers $\mathbb{Z}[\varphi]$ into $\mathbb{R}$. Elements are pairs $\langle a,b\rangle$ of integers, standing for $a+b\varphi$, with multiplication forced by the golden relation $\varphi^2=\varphi+1$. The evaluation map is defined by $\langle a,b\rangle\mapsto a+b\cdot\varphi_{\mathbb{R}}$, where $\varphi_{\mathbb{R}}$ is the classical positive golden ratio from PhiForcing.

The surrounding development keeps the T6 derivation (unique positive golden root) entirely inside $\mathbb{Z}[\varphi]$ at sigma0, then pays the continuum tax once at this boundary. Sibling facts show the map is a ring embedding and that the decidable integer sign predicate matches real positivity, so sigma0 uniqueness and trichotomy statements are about the real order, not a private surrogate.

One-line simp wrapper. Unfold the evaluation definition: the zero golden integer has integer coefficients $(0,0)$, so the real linear combination $0+0\cdot\varphi$ is definitionally $0$. No arithmetic lemmas are required.

Base case for every transport that compares against zero under the display map. Downstream it is used by the sign bridge (decidable positivity iff real positivity), the kernel fact (evaluation vanishes only at zero), nonnegativity of the recovered J-cost, and the transport of the Recognition Composition Law and the laws of logic (identity, non-contradiction, scale invariance) from recovered reals onto Mathlib reals. It also supports positivity of the recovered $\varphi$. In the forcing chain this sits at the T6 display step: sigma0 structure is shown to land on the classical PhiForcing presentation, with continuum choice confined to the display.