add_a
plain-language theorem explainer
On the golden ring ℤ[φ] ≅ ℤ×ℤ, addition acts componentwise on the integer part: the a-coefficient of x+y is x.a+y.a. Anyone rewriting ring operations or bridging to ℝ via toReal cites this. The proof is pure definitional equality (rfl).
Claim. Let $x,y\in\mathbb{Z}[\varphi]$ with $x=a_x+b_x\varphi$ and $y=a_y+b_y\varphi$. Then the integer coefficient of $x+y$ equals $a_x+a_y$.
background
GoldenInt is the ring $\mathbb{Z}[\varphi]$ realized as pairs $(a,b)\in\mathbb{Z}\times\mathbb{Z}$ for $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. The $a$-field is the pure integer part; the $b$-field is the coefficient of $\varphi$.
This module is the sigma0 (choice-free) re-derivation of the T6 golden-ratio forcing node. The classical spine proves uniqueness of the positive root of $x^2=x+1$ over $\mathbb{R}$ and pays a Classical.choice tax; here the same content is rebuilt by elementary integer arithmetic so the axiom closure stays inside ${propext, Quot.sound}$.
Component lemmas such as this one form the only allowed simp set in the module: full simp is banned because Mathlib's default set reaches choice-tainted lemmas.
proof idea
One-line definitional proof. Addition on GoldenInt is defined fieldwise on the structure, so the equality $(x+y).a = x.a + y.a$ holds by rfl. No lemmas are invoked.
why it matters
Feeds the component-lemma simp set used throughout GoldenInt (sibling mul_b and the other rfl projections). Downstream, GoldenIntReal.toReal_add applies it with add_b to show the real embedding preserves addition: toReal(x+y)=toReal x + toReal y, paying the continuum tax only at the display boundary.
In the Recognition forcing chain this supports the T6 node (φ as the self-similar fixed point) under the Delta Forcing Spectrum program: the ring laws needed for uniqueness and positivity of φ are established without reals, so the derivation itself is DELTA_FORCED rather than CHOICE-graded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.