toReal_eq_zero_iff
plain-language theorem explainer
The evaluation map from golden integers ℤ[φ] into ℝ has trivial kernel: a + bφ maps to zero iff a = b = 0. Anyone establishing the ring embedding of ℤ[φ] into the continuum cites this. The proof clears the φ-display, reduces vanishing to an integer equation s² = 5b², and applies the sigma0 irrationality descent.
Claim. For every golden integer $x = a + b\varphi$ with $a,b \in \mathbb{Z}$, the real evaluation $a + b\cdot\varphi_{\mathbb{R}}$ equals $0$ if and only if $x = 0$ in $\mathbb{Z}[\varphi]$.
background
The golden ring ℤ[φ] is the structure of pairs (a, b) of integers representing a + b·φ, with multiplication folded through the relation φ² = φ + 1. This module is the sigma1 display bridge: DeltaSpine.GoldenInt derives T6 (φ forced as the unique positive golden root) entirely inside ℤ[φ] at sigma0; GoldenIntReal pays the continuum tax once by evaluating into ℝ.
The evaluation map sends ⟨a, b⟩ to a + b·φ_ℝ, where φ_ℝ is the classical golden ratio (1 + √5)/2 from PhiForcing. The key upstream lemma is the integer irrationality descent: if s² = 5·b² for integers s, b, then b = 0. That fact is pure sigma0 number theory (no reals) and is the engine that forces the kernel of the display map to be trivial.
The converse direction is immediate from the simp fact that zero evaluates to zero.
proof idea
Bidirectional constructor. The reverse direction is the one-line simp toReal_zero.
Forward: assume a + b·φ_ℝ = 0. Substitute φ_ℝ = (1 + √5)/2 and clear denominators by linarith to obtain the real identity (2a + b) + b·√5 = 0. Rearrange to 2a + b = −b·√5, square both sides (using √5 · √5 = 5), and cast back to integers: (2a + b)² = 5·b². The sigma0 lemma int_sq_eq_five_sq forces b = 0; substituting back into the cleared identity forces a = 0. Conclude by extensionality on the GoldenInt pair.
why it matters
This is the kernel half of the ring embedding of ℤ[φ] into ℝ. The immediate parent is toReal_injective, which reduces injectivity to this statement via toReal_add and toReal_neg: if toReal x = toReal y then toReal(x − y) = 0, hence x − y = 0.
In the Recognition framework this closes the display half of T6. The forcing chain derives φ inside ℤ[φ] with only propext and Quot.sound; the continuum identification (toReal phi = PhiForcing.φ, and the positivity bridge isPos ↔ toReal > 0) needs a faithful embedding. Without trivial kernel the sigma0 uniqueness theorems would speak about a private surrogate order rather than the classical real order. The module doc is explicit: derivation is delta-forced; only display costs Classical.choice via Real.sqrt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.