five_dvd_of_five_dvd_sq

Module GoldenInt 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$, staying inside elementary integer arithmetic. The continuum carrier of the older PhiForcing spine is deliberately avoided so the axiom closure can sit in sigma0 (subset of {propext, Quot.sound}).

The multiplicative norm $N(a+b\varphi)=a^{2}+ab-b^{2}$ reduces the integral-domain property of this ring to the statement that no nonzero natural square is five times a square. That irrationality-of-$\sqrt{5}$ fact is proved by strong induction on $\mathbb{N}$; the present lemma is the prime-divisibility step that lets the induction descend.

Tactic hygiene is strict: case splits must be explicit rcases (not omega on a disjunctive goal), and omega/decide are used only to close atomic goals, keeping Classical.choice out of the proof term.

Unpack the hypothesis to a witness $c$ with $x\cdot x=5c$. Reduce via Nat.mul_mod to the atomic congruence $(x\bmod 5)^{2}\bmod 5=0$, closed by omega. Bound the residue by Nat.mod_lt. Then rcases on the value of $x\bmod 5$ into the six shapes $0,1,2,3,4,\ge 5$. Residue $0$ is exactly $5\mid x$. Residues $1$–$4$ each rewrite into the congruence and are absurd by decide (none of $1^{2},2^{2},3^{2},4^{2}$ is $0$ mod $5$). The $\ge 5$ branch contradicts the strict bound, closed by omega. No Euclid lemma and no classical case-split tactic is used.

Immediate parent is sq_ne_five_sq: no nonzero natural square equals five times a square, proved by strong induction whose divisibility step is exactly this lemma. That ℕ-level irrationality of $\sqrt{5}$ is the only non-ring ingredient needed for the norm argument that $\mathbb{Z}[\varphi]$ is an integral domain, which in turn lets the module state and prove “$\varphi$ is the unique positive root of $x^{2}=x+1$” with no real numbers.

In the forcing chain this is the sigma0 (DELTA_FORCED) re-derivation of T6: the self-similar fixed point $\varphi$ is forced by elementary arithmetic rather than by a choice-tainted continuum proof. The continuum tax is paid once later, at the display bridge in GoldenIntReal. Without this five-divisibility fact the descent for $\sqrt{5}$ fails and the choice-free T6 node does not close.