one_a
plain-language theorem explainer
In the golden ring ℤ[φ], the multiplicative unit has integer part 1. Anyone simplifying componentwise arithmetic on GoldenInt cites this. The proof is pure definitional equality (rfl).
Claim. If $1$ denotes the multiplicative identity of the golden ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ for $a+b\varphi$), then its integer coefficient equals $1$: $(1)_{a}=1$.
background
The module rebuilds the T6 golden-ratio forcing node over the discrete 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 choice-free (sigma0) derivation: only elementary integer arithmetic, no continuum carrier.
GoldenInt is the structure with fields $a$ (integer part) and $b$ ($\varphi$-coefficient). Ring operations are defined componentwise so that the unit is the pair $(1,0)$. Component projection lemmas such as this one form the restricted simp set used throughout the file; full simp is banned to avoid choice-tainted Mathlib lemmas.
proof idea
One-line definitional proof: rfl. By construction of the OfNat/One instance on GoldenInt, the unit is the pair with $a=1$ and $b=0$, so projecting the first component is definitionally $1$.
why it matters
Feeds the component simp set that powers every ring identity in the delta-spine. Downstream, golden_factorization rewrites $(x-\varphi)(x-\psi)=x^{2}-x-1$ by simp only over the component lemmas (including this one) plus ring on $\mathbb{Z}$. That factorization is the algebraic heart of the choice-free T6 node: the golden equation has exactly the two roots $\varphi$ and $\psi$ inside $\mathbb{Z}[\varphi]$.
In the Recognition forcing chain this supports the sigma0 re-derivation of T6 (phi as the self-similar fixed point) without paying the continuum/choice tax inside the derivation; the real embedding is deferred to GoldenIntReal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.