norm_zero
plain-language theorem explainer
The field norm on the golden integers vanishes at zero: N(0)=0. Anyone proving the integral-domain law or the kernel of N on ℤ[φ] cites this simp lemma. The proof is a one-shot decide on the integer formula a²+ab−b² at the zero pair.
Claim. Let $N:\mathbb{Z}[\varphi]\to\mathbb{Z}$ be the field norm $N(a+b\varphi)=a^2+ab-b^2$. Then $N(0)=0$.
background
GoldenInt is the choice-free carrier for the T6 golden-ratio node: the ring $\mathbb{Z}[\varphi]\cong\mathbb{Z}\times\mathbb{Z}$ with $(a,b)\mapsto a+b\varphi$ and multiplication reduced by $\varphi^2=\varphi+1$. The module re-derives the unique positive root of $x^2=x+1$ by elementary integer arithmetic, targeting axiom closure ${\mathrm{propext},\mathrm{Quot.sound}}$ (sigma0 DELTA_FORCED).
The norm is the multiplicative field norm $N(a+b\varphi)=a^2+ab-b^2$, equivalently the product with the conjugate $(a+b)-b\varphi$. It lands in $\mathbb{Z}$ and is the main tool for proving that $\mathbb{Z}[\varphi]$ is an integral domain without continuum or choice: later one rewrites $4N(x)=(2a+b)^2-5b^2$ and invokes irrationality of $\sqrt{5}$ by strong induction on $\mathbb{N}$.
proof idea
One-line tactic proof: by decide. Zero in GoldenInt is the pair $(0,0)$, so the defining polynomial $a^2+ab-b^2$ evaluates to the integer $0$, which Lean decides by computation. No lemmas are invoked; the @[simp] attribute makes the fact available to later simp only chains under the module's restricted simp hygiene.
why it matters
This is the base case that unlocks the multiplicative-norm route to the integral domain law. Downstream, mul_eq_zero_iff rewrites $N(x)N(y)=N(xy)=N(0)$ via norm_mul and this lemma, then splits on $\mathbb{Z}$ zero-divisors and applies norm_eq_zero_iff. That theorem in turn is where irrationality of $\sqrt{5}$ does the work ($4N(x)=(2a+b)^2-5b^2$).
In the Recognition forcing chain this supports the sigma0 re-derivation of T6 (phi as self-similar fixed point) inside DeltaSpine, keeping Classical.choice out of the golden-ring core. Geometry uses elsewhere that mention a norm_zero are ambient Euclidean norms; the GoldenInt consumers are the domain and kernel lemmas above.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.