norm
plain-language theorem explainer
Multiplicative field norm on golden integers: N(a + bφ) = a² + ab − b², the product with the conjugate (a+b) − bφ. Cited by anyone proving ℤ[φ] is an integral domain or running the choice-free T6 spine. One-line integer polynomial on the coefficient pair.
Claim. For $x = a + b\varphi$ in the golden ring $\mathbb{Z}[\varphi]$ (pairs of integers with multiplication folded through $\varphi^2 = \varphi + 1$), the field norm is the integer $N(x) = a^2 + ab - b^2$, equal to the product of $x$ with its conjugate $(a+b) - b\varphi$.
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\cdot\varphi$, with ring laws reduced to elementary integer arithmetic via $\varphi^2 = \varphi + 1$. The design target is sigma0 (axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$): no Classical.choice and no continuum carrier in the derivation.
The field norm is the standard number-field norm of $\mathbb{Q}(\sqrt{5})$ pulled back to integer coefficients. Module documentation states that the integral-domain property of $\mathbb{Z}[\varphi]$ reduces, via multiplicativity of $N(a+b\varphi) = a^2 + ab - b^2$, to the irrationality of $\sqrt{5}$, proved by strong-induction descent on $\mathbb{N}$. Positivity is handled separately by a decidable predicate on $(2a+b,b)$, so the unique-positive-root claim never mentions reals.
The structure GoldenInt supplies the two integer fields $a$ and $b$ that the formula reads.
proof idea
Pure definition: evaluate the integer polynomial $a^2 + ab - b^2$ on the coefficient pair of $x$. No lemmas, no tactics. The doc-comment identifies the same expression as the product against the conjugate $(a+b) - b\varphi$.
why it matters
This is the algebraic engine behind the choice-free T6 node. The module doc makes the reduction explicit: integral domain of $\mathbb{Z}[\varphi]$ factors through multiplicativity of this norm down to irrationality of $\sqrt{5}$. Downstream, Algebra.PhiRing.PhiInt reuses the same coefficient pair and norm pattern; phi_ring_certificate and Constants.GapWeight consume it for ring and mass-ladder bookkeeping. In the forcing chain it supports the sigma0 re-derivation of T6 (φ as self-similar fixed point) without paying the continuum tax until the display bridge in GoldenIntReal. About forty use sites hang off this single formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.