toReal_injective
plain-language theorem explainer
The evaluation map from golden integers ℤ[φ] into ℝ is injective, so distinct integer pairs (a,b) give distinct reals a+bφ. Anyone building the ring embedding of the sigma0 golden integers into the continuum cites this. The proof reduces injectivity to a trivial kernel via the zero characterization, then cancels by adding the second argument.
Claim. The evaluation $\mathrm{ev}:\mathbb{Z}[\varphi]\to\mathbb{R}$ given by $\langle a,b\rangle\mapsto a+b\varphi$ is injective: if $\mathrm{ev}(x)=\mathrm{ev}(y)$, then $x=y$ as golden integers.
background
The module GoldenIntReal is the display bridge from the discrete golden integers ℤ[φ] into ℝ. Upstream, DeltaSpine.GoldenInt derives T6 (φ forced as the unique positive golden root) entirely inside ℤ[φ] with only {propext, Quot.sound}. This module pays the continuum tax once: it evaluates pairs into reals and shows the sigma0 structure matches the classical PhiForcing presentation.
The evaluation is toReal ⟨a,b⟩ = a + b·φ, with φ the classical golden ratio from PhiForcing. Additivity (toReal_add) and negation (toReal_neg) are immediate from the coordinate formulas. The key upstream fact is toReal_eq_zero_iff: the kernel is trivial, because a + bφ = 0 forces a = b = 0 by the irrationality descent int_sq_eq_five_sq (equivalently, √5 irrational). That lemma is the only place the continuum enters the injectivity argument.
proof idea
Standard kernel argument for additive maps. From toReal x = toReal y, form the difference: toReal (x + (-y)) = 0 by toReal_add, toReal_neg, and a one-line ring rewrite. Apply toReal_eq_zero_iff to conclude x + (-y) = 0 in GoldenInt. Congruence by adding y on the right, then simpa with add_assoc, add_comm, and add_left_comm yields x = y. No continuum reasoning appears in this proof itself; it is all inherited from the zero characterization.
why it matters
Injectivity is the missing half of the ring embedding: together with toReal_add, toReal_mul, and the unit maps, it shows ℤ[φ] sits inside ℝ as a subring. The module doc lists this as part of the sigma1 display package that makes the sigma0 T6 derivation speak about the classical golden ratio (1+√5)/2 rather than a private surrogate.
Downstream the embedding underwrites the sign bridge (isPos_iff_toReal_pos) and the T6 bridge theorem that the unique positive golden root evaluates to the classical φ. In the Recognition forcing chain this is the continuum readout of T6 (φ forced as self-similar fixed point), not a new forcing step. No used_by edges are recorded yet; the lemma is infrastructure for any later uniqueness or positivity transfer that needs faithful display into ℝ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.