norm_mul
plain-language theorem explainer
The field norm on the golden integers is multiplicative: N(xy)=N(x)N(y) for all x,y in Z[φ]. Cited by anyone proving the integral-domain law, the φ-ring certificate, or phase invariance of J-cost via modulus. Proof is pure integer algebra: unfold the two multiplication components and close with ring over Z.
Claim. For all $x,y\in\mathbb{Z}[\varphi]$, writing $N(a+b\varphi)=a^{2}+ab-b^{2}$, one has $N(xy)=N(x)\,N(y)$.
background
GoldenInt is the ring $\mathbb{Z}[\varphi]$ realized as pairs $(a,b)$ for $a+b\varphi$, with multiplication folded through the relation $\varphi^{2}=\varphi+1$. Explicitly, $(xy){a}=x{a}y_{a}+x_{b}y_{b}$ and $(xy){b}=x{a}y_{b}+x_{b}y_{a}+x_{b}y_{b}$.
The norm is the field norm $N(a+b\varphi)=a^{2}+ab-b^{2}$, equal to the product with the Galois conjugate $(a+b)-b\varphi$. This module re-derives the T6 golden-ratio forcing node over elementary integer arithmetic (sigma0, no Classical.choice), rather than over $\mathbb{R}$ with $\sqrt{5}$.
Multiplicativity of $N$ is the algebraic engine behind the integral-domain property: $xy=0$ forces $N(x)N(y)=0$, hence a factor vanishes after the irrationality of $\sqrt{5}$ is established by descent on $\mathbb{N}$.
proof idea
One-line tactic proof. Unfold norm and the two component lemmas for multiplication (mul_a, mul_b), which are definitional (rfl). The resulting equality of integer polynomials is closed by ring over $\mathbb{Z}$. No induction, no case splits, no real numbers.
why it matters
This is item 4 of the φ-ring certificate: the formal checklist that $\mathbb{Z}[\varphi]$ carries ring operations, conjugation, multiplicative norm, and the defining relation $\varphi^{2}=\varphi+1$. Downstream, mul_eq_zero_iff uses it to get the integral-domain law on GoldenInt.
It also feeds the ComplexStructureForcing phase-invariance suite (jcost_phase_invariant, jcost_modulus_only, mode_cost_phase_invariant), where multiplicativity of the complex modulus (same algebraic shape) shows J-cost depends only on $|\psi|$, the structural root of the Born rule. In the forcing chain this sits under T6 (φ forced as the self-similar fixed point), now re-proved choice-free on the delta spine.
The Algebra.PhiRing layer reuses the same identity for its parallel PhiInt formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.