toReal_two
plain-language theorem explainer
The integer 2, viewed as an element of the golden ring ℤ[φ], evaluates under the display map to the ordinary real 2. Anyone relating discrete sigma0 costs (traces, doubled J) to classical real J-cost cites this. The proof identifies 2 with the pair ⟨2,0⟩ and reduces the evaluation to a trivial cast-and-ring identity.
Claim. Under the evaluation map $\mathbb{Z}[\varphi]\to\mathbb{R}$ sending $a+b\varphi$ to $a+b\varphi_{\mathbb{R}}$, the ring element $2$ satisfies $\mathrm{eval}(2)=2$.
background
The module GoldenIntReal is the sigma1 display bridge from the discrete golden ring ℤ[φ] into ℝ. GoldenInt is the structure of pairs ⟨a,b⟩ standing for a + b·φ, with multiplication folded through the relation φ² = φ + 1. The evaluation map toReal sends ⟨a,b⟩ to a + b·PhiForcing.φ on the classical reals.
Upstream, T6 forces φ as the unique positive golden root entirely inside ℤ[φ] (sigma0, axiom closure {propext, Quot.sound}). This module pays the continuum cost once: Real.sqrt and real arithmetic appear only at the display boundary. Sibling facts already record toReal 0 = 0, toReal 1 = 1, and toReal φ = PhiForcing.φ.
The integer 2 embeds as ⟨2,0⟩, so its image is the pure integer part with vanishing φ-coefficient. That elementary identity is needed whenever discrete expressions subtract 2 (traces, doubled costs) and must match classical formulas written with the real number 2.
proof idea
Tactic proof in four short steps. First, decide establishes that the GoldenInt literal 2 equals the pair ⟨2, 0⟩. Rewrite with that equality, then unfold toReal to the goal (2 : ℤ) + (0 : ℤ)·φ = 2 on ℝ. push_cast clears the integer-to-real coercions; ring finishes the arithmetic. No external lemmas beyond the definition of toReal and the structure of GoldenInt.
why it matters
Feeds directly into jdouble_eq_jcost, the J-cost display theorem: the sigma0 doubled cost Jdouble n evaluates to 2·Jcost(φⁿ) for the canonical cost J(x) = (x + x⁻¹)/2 − 1. That proof rewrites toReal(traceZ n − 2) and invokes toReal_two to match the classical −1 shift inside Jcost.
In the Recognition framework this is a small but load-bearing bridge step. The discrete Recognition Composition Law is proved at sigma0 inside ℤ[φ]; the continuum uniqueness of J (T5, forcing chain) lives on ℝ. Aligning the constant 2 on both sides lets the discrete RCL display as the functional equation that forces Jcost in Cost.FunctionalEquation. Without it, the doubled-cost comparison would carry an unresolved integer-versus-real mismatch.
No open scaffolding: the claim is fully proved. It sits in the honest sigma1 CHOICE layer (display only), while the derivation it serves remains delta-forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.