toReal_phi

The module is the sigma1 display boundary for the golden ring. Upstream, GoldenInt is the structure of pairs $(a,b)\in\mathbb{Z}^2$ representing $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. T6 (φ forced as the unique positive golden root) is derived entirely inside that ring at sigma0, with axiom closure limited to propext and Quot.sound.

Here the continuum tax is paid once: the evaluation map sends $\langle a,b\rangle$ to $a+b\cdot\varphi_{\mathbb{R}}$, where $\varphi_{\mathbb{R}}$ is the classical positive root from the PhiForcing presentation. The module's job is to show that the sigma0 structure lands on that classical object, so later real inequalities and order facts are about the ordinary golden ratio, not a private surrogate.

One-line simp unfolding the evaluation definition and the golden-ring generator. The generator is the pair with integer part $0$ and $\varphi$-coefficient $1$, so the map reduces immediately to $0+1\cdot\varphi_{\mathbb{R}}$, which is definitionally the classical root.

This is the atomic identification that every continuum readout of discrete golden arithmetic depends on. Downstream, the T6 display bridge rewrites through it to conclude that the unique positive sigma0 golden root equals $(1+\sqrt{5})/2$, is positive, and satisfies $x^2=x+1$. The inverse and integer-power ladder theorems reuse it to send $\varphi^{-1}$ and $\varphi^n$ to their classical real counterparts. The ladder-ratio display bridge then translates sigma0 rational brackets on $\varphi$, $\varphi^5$, and $\varphi^8$ into genuine real inequalities used in continuum constants work.

In the forcing chain this closes the display half of T6: φ is forced inside ℤ[φ]; only the map into ℝ costs classical choice. Without the equality, sigma0 uniqueness would remain sealed off from Mathlib reals and from the alpha-band and mass-ladder readouts that quote classical φ.