one_b
plain-language theorem explainer
In the golden ring ℤ[φ] ≅ ℤ×ℤ, the multiplicative unit is the pair (1,0), so its φ-coefficient is 0. Anyone rewriting componentwise ring arithmetic on ℤ[φ] cites this as part of the banned-full-simp component lemma set. The proof is pure definitional equality (rfl).
Claim. Writing elements of the golden ring as $a+b\varphi$ with $a,b\in\mathbb{Z}$, the multiplicative identity is $1+0\cdot\varphi$, hence 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)$ standing for $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: only {propext, Quot.sound}, no Classical.choice.
GoldenInt is the structure with integer fields a (rational part) and b ($\varphi$-coefficient). The unit of the ring is definitionally the pair with $a=1$ and $b=0$. Component projection lemmas such as this one form the only allowed simp set in the module; full simp is banned because Mathlib's default simp set pulls in choice-tainted material.
proof idea
One-line definitional proof: rfl. The multiplicative identity on GoldenInt is constructed so that its second field is the integer 0, and the statement is exactly that field projection.
why it matters
This is one atom of the component-lemma simp set that every later rewrite in the module is required to use. Downstream, mul_b records the $\varphi$-coefficient of a product, and golden_factorization expands $(x-\varphi)(x-\psi)=x^2-x-1$ by ext plus simp only over the component lemmas (including this one) followed by ring on $\mathbb{Z}$.
That factorization is the algebraic heart of the choice-free T6 node: the golden polynomial has exactly the two roots $\varphi$ and $\psi$ inside $\mathbb{Z}[\varphi]$. The continuum bridge (toReal) is deferred to a separate sigma1 module, so the forcing content itself stays delta-forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.