toReal
plain-language theorem explainer
Evaluation map from the golden integer ring ℤ[φ] into ℝ, sending the pair (a, b) to a + b·φ with the classical golden ratio. Anyone bridging the sigma0 derivation of φ into continuum display cites this map. The body is the direct linear combination; no proof content beyond the formula.
Claim. Define the evaluation $\mathbb{Z}[\varphi]\to\mathbb{R}$ by $\langle a,b\rangle\mapsto a + b\cdot\varphi$, where $\varphi$ is the classical positive golden ratio and $a,b\in\mathbb{Z}$.
background
The golden ring ℤ[φ] is the structure of integer pairs (a, b) standing for a + b·φ, with multiplication folded through the relation φ² = φ + 1. T6 (φ forced as the unique positive golden root) is derived entirely inside that ring under a tight axiom closure; the continuum is not used there.
This module is the single display boundary: it evaluates ℤ[φ] into Mathlib ℝ and shows the sigma0 structure maps onto the classical PhiForcing presentation of φ. The evaluation uses the classical real golden ratio from PhiForcing, so the continuum cost (Classical.choice via Real.sqrt and real arithmetic) is paid exactly once at display, not in the derivation.
Sibling facts then show the map is a ring embedding, sends the sigma0 generator to classical φ, and identifies the decidable integer positivity predicate with real positivity.
proof idea
Pure definition: cast the integer coefficients to ℝ and form the linear combination a + b·φ with the classical golden ratio. No lemmas, no tactics; noncomputable only because the ambient real φ is.
why it matters
This is the sigma1 display bridge that lets continuum consumers read sigma0 results about ℤ[φ]. Downstream, the cost layer uses it to transport the recovered-real J-cost and the Recognition Composition Law onto the classical real statements (nonnegativity, symmetry, zero locus, square formula, composition law). Algebra.PhiRing rebuilds the same pair type as PhiInt on top of this evaluation.
In the forcing chain it closes the T6 display: the unique positive golden root forced inside ℤ[φ] evaluates to (1+√5)/2. Without this map, sigma0 uniqueness and trichotomy would remain private to the integer ring rather than statements about the real order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.