add_b
plain-language theorem explainer
Component projection for addition in the golden ring ℤ[φ]: the φ-coefficient of a sum is the sum of the φ-coefficients. Anyone rewriting ring arithmetic or bridging to ℝ via toReal cites this simp lemma. The proof is pure definitional equality (rfl) from componentwise addition on pairs.
Claim. For all $x,y$ in the golden ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ meaning $a+b\varphi$), the $\varphi$-coefficient of $x+y$ equals the sum of the $\varphi$-coefficients of $x$ and $y$.
background
The module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$, so the derivation stays inside ${propext, Quot.sound}$ (sigma0 DELTA_FORCED). Elements are pairs $(a,b)\in\mathbb{Z}\times\mathbb{Z}$ standing for $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$.
Addition is the product ring law on pairs: $(a_1,b_1)+(a_2,b_2)=(a_1+a_2,b_1+b_2)$. The companion projection for the integer part is the sibling lemma on the $a$-component. Full simp is banned in this file (choice contamination from Mathlib's default simp set); only these component rfl lemmas plus ring over $\mathbb{Z}$ are used.
proof idea
One-line definitional proof: rfl. Once addition on GoldenInt is defined by adding the two integer fields separately, the equality of $b$-components is judgmentally true and needs no further lemmas.
why it matters
Part of the component-lemma simp set that keeps every later rewrite choice-free. Downstream, mul_b sits beside it in that set, and toReal_add in GoldenIntReal applies both projections (simp only [toReal, add_a, add_b]) to show the real embedding preserves addition before paying the continuum tax once at the display boundary.
That boundary is how the sigma0 spine reconnects to the classical T6 node in PhiForcing (unique positive root of $x^2=x+1$) without smuggling Classical.choice into the forcing chain itself. The landmark is T6: $\varphi$ as the self-similar fixed point, re-derived here by elementary integer arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.