mul_eq_zero_iff
plain-language theorem explainer
The golden ring ℤ[φ] is an integral domain: a product of two elements vanishes if and only if one factor is zero. Anyone proving uniqueness of roots of the golden equation over ℤ[φ] cites this. The argument multiplies through the multiplicative norm, reduces to ℤ being an integral domain, and recovers vanishing of each factor from the norm-zero criterion.
Claim. For all $x, y$ in the golden ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ representing $a + b\varphi$ with multiplication folded through $\varphi^2 = \varphi + 1$), one has $x \cdot y = 0$ if and only if $x = 0$ or $y = 0$.
background
This module re-derives the T6 golden-ratio forcing node over the 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 reduced by the relation $\varphi^2 = \varphi + 1$. The goal is a choice-free (sigma0) development: only elementary integer arithmetic, no continuum carrier tax.
The field norm $N(a + b\varphi) = a^2 + ab - b^2$ is multiplicative and equals the product with the conjugate $(a+b) - b\varphi$. Upstream, norm_eq_zero_iff records that $N(x)=0$ forces $x=0$, via the identity $4N(x)=(2a+b)^2 - 5b^2$ and the irrationality of $\sqrt{5}$ proved by strong induction on $\mathbb{N}$. Multiplicativity $N(xy)=N(x)N(y)$ and $N(0)=0$ are already available.
Together these make the integral-domain property a pure transfer from $\mathbb{Z}$ through the norm, without invoking real embeddings or classical choice.
proof idea
Bidirectional constructor.
Forward: from $xy=0$, multiplicativity gives $N(x)N(y)=N(xy)=N(0)=0$. Since $\mathbb{Z}$ is an integral domain, $N(x)=0$ or $N(y)=0$. Apply norm_eq_zero_iff on each branch to conclude $x=0$ or $y=0$.
Reverse: case-split on $x=0$ or $y=0$; both sides are immediate by componentwise extension and the ring simplifier (golden_simp plus ring).
why it matters
This is the integral-domain lemma that lets the golden equation factor cleanly inside $\mathbb{Z}[\varphi]$. Downstream, golden_roots uses it exactly once: after writing $(x-\varphi)(x-\psi)=0$ from the golden factorization identity, the domain property yields $x=\varphi$ or $x=\psi$, with no quadratic formula and no Real.sqrt.
In the Recognition forcing chain this closes the algebraic half of T6 (phi forced as the self-similar fixed point) at sigma0: the axiom footprint stays inside {propext, Quot.sound}. The continuum bridge (toReal, positivity comparison with the real $\varphi$) is deferred to GoldenIntReal and paid once at the display boundary. Without this lemma the choice-free uniqueness of the two golden roots would not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.