phi_sq

The module re-derives the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi] \cong \mathbb{Z}\times\mathbb{Z}$, with pairs $(a,b)$ read as $a + b\varphi$ and multiplication reduced by the relation $\varphi^2 = \varphi + 1$. The goal is a sigma0 (DELTA_FORCED) axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$, avoiding Classical.choice and the continuum carrier used by the older real-analytic spine node.

Here $\varphi$ is the ring unit of the second coordinate (the formal generator). The same identity appears elsewhere over $\mathbb{R}$ (via $\sqrt{5}$ and nlinarith, or via a constants package), but those proofs sit at higher forcing grade. This declaration is the elementary integer form that the delta-spine can audit without reals.

One-line tactic proof: decide. After unfolding the GoldenInt multiplication (which folds the second-coordinate product through the golden relation on integer literals), both sides reduce to equal pairs of integers, and the kernel closes the equality by computation. No lemmas are invoked beyond the ring's definitional arithmetic.

First conjunct of t6_delta_forced, the sigma0 packaging of T6: φ satisfies the golden self-similarity equation, is positive in the decidable sign structure, and is the unique positive root among the two roots φ and ψ = 1 − φ. That theorem is the choice-free replacement for the continuum uniqueness statement in the forcing chain (T6: φ forced as the self-similar fixed point).

Downstream, the display bridge theorem only evaluates this identity under toReal, recovering the classical $(1+\sqrt{5})/2$ without redoing uniqueness. The same equation is also a field of the NumberTheoryCert structure (with the Fibonacci ladder identities for $\varphi^5$ and $\varphi^8$). Without this atomic fact, the delta-spine cannot claim T6 inside the audited axiom set.