int_sq_eq_five_sq
plain-language theorem explainer
If two integers satisfy s² = 5 b², then b must be zero. This is the ℤ-level form of √5-irrationality used throughout the choice-free golden ring ℤ[φ]. Anyone proving that the GoldenInt norm is zero only at zero, or that positivity is trichotomous, cites it. The proof lifts the equation to natural absolute values and applies the ℕ descent lemma sq_ne_five_sq.
Claim. For all integers $s,b$, if $s^2 = 5 b^2$, then $b = 0$.
background
The module GoldenInt rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi] \cong \mathbb{Z}\times\mathbb{Z}$ with $(a,b)\mapsto a+b\varphi$ and multiplication folded by $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: only {propext, Quot.sound}, no continuum and no Classical.choice.
The field norm is $N(a+b\varphi)=a^2+ab-b^2$, the product with the conjugate. Integral-domain and positivity facts reduce to the arithmetic statement that no nonzero square is five times a square. The ℕ form of that fact is already proved by strong induction as sq_ne_five_sq. The present lemma is the integer packaging: $s^2=5b^2$ forces $b=0$.
Positivity of $a+b\varphi$ is encoded by a decidable predicate on the pair $(s,t)=(2a+b,b)$, the exact sign trichotomy of $s+t\sqrt{5}$. The tie case $s^2=5t^2$ is exactly what this lemma kills.
proof idea
Apply natAbs to both sides of $s\cdot s=5\cdot(b\cdot b)$ to obtain an equality of natural numbers. Multiplicativity of Int.natAbs rewrites the right-hand side as $5\cdot b.\mathrm{natAbs}^2$ (using (5:ℤ).natAbs=5). The ℕ descent theorem sq_ne_five_sq then yields $b.\mathrm{natAbs}=0$, hence $b=0$ via Int.natAbs_eq_zero. No induction is redone here; the work is pure transport from ℤ to ℕ.
why it matters
This is the integer hinge on which the sigma0 golden ring stands. Downstream, norm_eq_zero_iff rewrites $4N(x)=(2a+b)^2-5b^2$ and invokes this lemma to conclude $N(x)=0\Leftrightarrow x=0$, so $\mathbb{Z}[\varphi]$ is an integral domain without reals. The same exclusion of the tie $s^2=5b^2$ feeds isPos_trichotomy (exactly one of IsPos $x$, $x=0$, IsPos $(-x)$) and the pair-level exclusivity facts.
On the display bridge, GoldenIntReal.toReal_eq_zero_iff imports the same irrationality so that the real embedding kills only zero. Together these close the choice-free half of T6: $\varphi$ is forced as the unique positive root of $x^2=x+1$ inside $\mathbb{Z}[\varphi]$, with continuum tax paid once at the Real boundary. Framework landmark: T6 phi fixed point in the UnifiedForcingChain, re-derived as DELTA_FORCED.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.