toReal_psi
plain-language theorem explainer
The conjugate golden root ψ inside ℤ[φ] evaluates under the real embedding to 1 − φ. Anyone bridging the sigma0 golden-integer derivation to classical real arithmetic cites this identity. The proof is a one-line simp-and-ring reduction from the definitions of the embedding and of ψ as the pair (1, −1).
Claim. Under the evaluation map $a + b\varphi \mapsto a + b\varphi_{\mathbb{R}}$ from the golden integers into $\mathbb{R}$, the conjugate root $\psi := \langle 1,-1\rangle$ (i.e. $1-\varphi$) satisfies $\mathrm{toReal}(\psi) = 1 - \varphi$, where $\varphi$ is the classical golden ratio.
background
The module is the display bridge from the golden ring $\mathbb{Z}[\varphi]$ into $\mathbb{R}$. GoldenInt is the structure of pairs $(a,b)$ representing $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. Inside that ring the conjugate root is the pure definition $\psi:=\langle 1,-1\rangle$, i.e. $1-\varphi$.
The evaluation map sends $\langle a,b\rangle$ to $a+b\cdot\varphi_{\mathbb{R}}$ using the classical golden ratio from PhiForcing. As the module doc states, the sigma0 derivation of T6 ($\varphi$ forced as the unique positive golden root) lives entirely in $\mathbb{Z}[\varphi]$ with axiom closure ${\mathrm{propext},\mathrm{Quot.sound}}$; only the display into the continuum costs Classical.choice.
Sibling facts record the images of $0$, $1$, and $\varphi$ itself, the ring-homomorphism laws, and the bridge that the unique positive golden root evaluates to $(1+\sqrt{5})/2$.
proof idea
One-line wrapper. Unfold the evaluation map and the definition $\psi=\langle 1,-1\rangle$ by simp, obtaining the real expression $1+(-1)\cdot\varphi$. Finish with ring to rewrite as $1-\varphi$.
why it matters
Records the real image of the algebraic conjugate of the golden root, so the sigma0-to-continuum display is honest on both roots of $x^2=x+1$. The conjugate is classically $(1-\sqrt{5})/2$; the theorem states the intermediate form $1-\varphi$ that matches the integer-pair definition.
This sits in the Foundation forcing layer that supports T6 ($\varphi$ forced as the self-similar fixed point). The module's larger job is to show the delta-forced golden-integer structure maps onto the classical PhiForcing presentation, including toReal phi = PhiForcing.φ and the positivity bridge isPos_iff_toReal_pos. No downstream users are recorded yet; the lemma is available wherever an argument needs the conjugate under the embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.