zero_b
plain-language theorem explainer
The φ-coefficient of the additive identity in the golden ring ℤ[φ] is zero. Anyone rewriting ring operations componentwise on pairs (a,b) cites this as part of the local simp set. The proof is pure definitional reflexivity from the Zero instance on the structure.
Claim. If $0$ denotes the additive identity of the golden ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ for $a+b\varphi$), then its $\varphi$-coefficient equals $0$.
background
The module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. 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$. The goal is a sigma0 (choice-free) derivation: axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$, with continuum display deferred to a separate bridge module.
GoldenInt is the structure with integer fields $a$ (rational part) and $b$ ($\varphi$-coefficient). Additive zero is the pair $(0,0)$. Component projections are the primitive data of every later ring-law lemma; the module bans full simp and only rewrites through a curated set of rfl component equalities plus ring on $\mathbb{Z}$.
proof idea
One-line wrapper: rfl. The Zero instance on GoldenInt sets both fields to $0$, so projecting .b is definitionally equal to the integer $0$. No lemmas are applied.
why it matters
Feeds the component simp set used by mul_b (and the rest of the ring API): multiplication of pairs expands as $(xy).b = x.a,y.b + x.b,y.a + x.b,y.b$, and zero-coefficient reductions are the base cases of that expansion. In the Delta Forcing Spectrum program this is scaffolding for the choice-free T6 node: unique positive root of $x^2=x+1$ stated entirely inside $\mathbb{Z}[\varphi]$, without Real.sqrt or classical choice. Landmark link: T6 $\varphi$ as the self-similar fixed point, re-derived on the integer carrier rather than the continuum spine Foundation.PhiForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.