toReal_mul
plain-language theorem explainer
Evaluation from the golden integers ℤ[φ] into ℝ is a ring homomorphism on products: toReal(x·y) equals the ordinary real product. Anyone moving discrete identities (unit ladder, inverse of φ, RCL transport) across the sigma0/sigma1 boundary cites this. The proof expands both sides componentwise and cancels the leftover φ²−φ−1 term by the defining equation of φ.
Claim. For all $x,y\in\mathbb{Z}[\varphi]$ (pairs of integers representing $a+b\varphi$), the evaluation map $\mathrm{ev}(a+b\varphi)=a+b\varphi_{\mathbb{R}}$ is multiplicative: $\mathrm{ev}(x\cdot y)=\mathrm{ev}(x)\,\mathrm{ev}(y)$. Multiplication on the left uses the folded law through $\varphi^{2}=\varphi+1$.
background
The module GoldenIntReal is the single continuum display bridge out of the discrete golden ring. Upstream, GoldenInt is the structure of pairs $(a,b)\in\mathbb{Z}^{2}$ standing for $a+b\varphi$, with multiplication folded by $\varphi^{2}=\varphi+1$: the product components are $(xy)_a=x_a y_a+x_b y_b$ and $(xy)_b=x_a y_b+x_b y_a+x_b y_b$ (the simp lemmas mul_a, mul_b).
Evaluation toReal sends $a+b\varphi$ to the classical real $a+b\varphi_{\mathbb{R}}$. The classical identity $\varphi^{2}=\varphi+1$ is PhiForcing.phi_equation (also available from PhiRing). The whole module is honestly sigma1 (Real.sqrt, nlinarith); the discrete T6 derivation stays sigma0, and only this display pays Classical.choice.
Sibling facts already record that toReal preserves $0$, $1$, $\varphi$, addition, and negation. Multiplicativity is the remaining ring-homomorphism clause before injectivity (via irrationality of $\sqrt{5}$).
proof idea
Tactic proof, three steps. First simp only [toReal, mul_a, mul_b] expands both sides into integer components cast to ℝ. Then push_cast normalizes the ℤ→ℝ coercions. The residual polynomial identity is exactly the discrepancy coming from treating $\varphi^{2}$ as free versus as $\varphi+1$; it is discharged by linear_combination against (-(x.b:ℝ)*(y.b:ℝ)) * PhiForcing.phi_equation. No induction, no case split: pure algebraic cancellation from the defining equation of φ.
why it matters
This is the multiplicative half of the ring embedding that lets sigma0 structure speak classical real language. Downstream it is used by toReal_phiInv (σ0 inverse φ−1 evaluates to real φ⁻¹), by toReal_phiZpow (the unit-group ladder becomes real integer powers of φ), and by t6_bridge (the unique positive golden root of the sigma0 derivation displays as $(1+\sqrt{5})/2$).
Further out, Cost.JcostLogic.compositionLawL_to_real transports a recovered-real composition law across toReal, so the Recognition Composition Law can be stated on classical costs. A parallel simp lemma in RealsFromLogic reuses the same pattern for the logic-real layer. In the forcing chain this sits under T6 (φ forced as the self-similar fixed point): the discrete uniqueness work is already done; this lemma only guarantees the product law survives the display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.