sq_ne_five_sq
plain-language theorem explainer
No nonzero natural number square equals five times a square: if m² = 5 n² over ℕ then n = 0. This is the elementary descent form of √5 irrationality used to prove the multiplicative norm on ℤ[φ] is an integral domain. Anyone citing the choice-free T6 golden-ratio forcing node needs it. The proof is strong induction on n, peeling factors of 5 via the five-divides-a-square lemma and closing with atomic omega.
Claim. For all natural numbers $n$ and $m$, if $m^2 = 5 n^2$ then $n = 0$. Equivalently, no nonzero natural square is five times a square (irrationality of $\sqrt{5}$ at the $\mathbb{N}$ level).
background
The module re-derives the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi] \cong \mathbb{Z}\times\mathbb{Z}$ with multiplication folded through $\varphi^2 = \varphi + 1$, entirely in elementary integer arithmetic. The goal is a sigma0 (choice-free) closure: only {propext, Quot.sound}, no Classical.choice. The continuum display of $\varphi$ is deferred to a separate bridge module.
The integral-domain property of this ring reduces, via the multiplicative norm $N(a+b\varphi) = a^2 + ab - b^2$, to the statement that $\sqrt{5}$ is irrational. The present theorem is the pure $\mathbb{N}$ form of that fact. The sole nontrivial upstream lemma is that five divides a square only through its root: if $5 \mid x^2$ then $5 \mid x$, proved by an explicit five-way residue split on $x \bmod 5$ (not by a choice-tainted omega disjunction).
proof idea
Strong induction on $n$ via Nat.strong_induction_on. Fix $m$ with $m^2 = 5 n^2$. If $n = 0$ we are done. Otherwise apply the upstream five-divides-a-square lemma to get $5 \mid m$, write $m = 5k$, and rearrange by ring plus atomic omega to $n^2 = 5 k^2$. Apply the same lemma to $n$ to get $5 \mid n$, write $n = 5j$, and rearrange again to $k^2 = 5 j^2$. The inequality $j < n$ is atomic omega, so the inductive hypothesis yields $j = 0$, hence $n = 0$, contradiction. No classical case analysis beyond by_cases n = 0.
why it matters
This is the arithmetic engine behind the choice-free T6 node in the Delta Forcing Spectrum program. Downstream, int_sq_eq_five_sq lifts the statement to integers: $s^2 = 5 b^2$ over $\mathbb{Z}$ forces $b = 0$, by reducing absolute values to the natural case and invoking this theorem. That integer form feeds the norm argument that $\mathbb{Z}[\varphi]$ is an integral domain, which in turn supports positivity and uniqueness facts (including that a positive golden integer is nonzero) used in the delta-forced T6 theorem.
In the forcing chain, T6 forces $\varphi$ as the self-similar fixed point. The classical spine proves T6 over $\mathbb{R}$ with Real.sqrt 5 and pays a Classical.choice tax; this descent lemma is what lets the GoldenInt module discharge the same content at sigma0. Without it the norm would not separate zero, and the ring-theoretic uniqueness of the positive root of $x^2 = x + 1$ would not close choice-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.