norm_eq_zero_iff
plain-language theorem explainer
The field norm on the golden ring ℤ[φ] vanishes if and only if its argument is zero. Anyone proving that ℤ[φ] is an integral domain cites this as the kernel step. The proof rewrites 4N(x)=(2a+b)²−5b², invokes the integer irrationality of √5 to force the φ-coefficient to zero, then recovers the integer part by a choice-free square-zero argument.
Claim. For every $x = a + b\varphi$ in the golden ring $\mathbb{Z}[\varphi]$, the field norm $N(x) = a^2 + ab - b^2$ satisfies $N(x) = 0$ if and only if $x = 0$.
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)$ standing for $a + b\varphi$, with multiplication folded through the relation $\varphi^2 = \varphi + 1$. The goal is a sigma0 (choice-free) derivation: every theorem must close inside ${\mathrm{propext},\mathrm{Quot.sound}}$.
The field norm is $N(a+b\varphi) = a^2 + ab - b^2$, the product of $x$ with its conjugate. It is multiplicative by pure ring arithmetic over $\mathbb{Z}$. The key arithmetic input is the integer form of the irrationality of $\sqrt{5}$: if $s^2 = 5b^2$ in $\mathbb{Z}$, then $b = 0$ (proved by strong-induction descent on $\mathbb{N}$). The identity $4N(x) = (2a+b)^2 - 5b^2$ converts a vanishing-norm hypothesis into exactly that Diophantine equation.
proof idea
Bidirectional constructor. The reverse direction is the one-line fact $N(0)=0$.
Forward: from $N(x)=0$, expand $(2a+b)^2$ by ring to obtain $(2a+b)^2 = 4N(x) + 5b^2$. Substituting the hypothesis yields $(2a+b)^2 = 5b^2$. The upstream lemma int_sq_eq_five_sq forces $b=0$. Substituting $b=0$ into $N(x)=0$ leaves $a^2=0$; omega closes the atomic equality, and the choice-free Int.mul_eq_zero splits $a\cdot a=0$ to $a=0$. Extensionality of the pair structure finishes $x=0$.
why it matters
This is the kernel step for the integral-domain theorem on $\mathbb{Z}[\varphi]$: the immediate parent mul_eq_zero_iff multiplies norms, applies Int.mul_eq_zero, and invokes this lemma on each factor. That domain property is the algebraic backbone of the sigma0 re-derivation of T6 (phi forced as the unique positive self-similar fixed point) inside the Delta Forcing Spectrum program.
By routing uniqueness of the positive root of $x^2=x+1$ through elementary integer arithmetic rather than Real.sqrt 5, the module keeps Classical.choice out of the forcing chain until the optional display bridge to $\mathbb{R}$. The irrationality of $\sqrt{5}$ is exactly the arithmetic content that makes the norm nondegenerate, so the lemma is where that number-theoretic fact enters the Recognition foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.