golden_factorization
plain-language theorem explainer
In the golden ring ℤ[φ], the monic quadratic x² − x − 1 factors as (x − φ)(x − ψ) for every ring element x. Anyone proving uniqueness of roots of the golden equation over ℤ[φ] cites this identity. The proof expands both sides on the integer components via the ring's a/b projections and closes with ordinary integer ring arithmetic.
Claim. For every $x$ in the golden integer ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ standing for $a+b\varphi$), one has $(x-\varphi)(x-\psi)=x^{2}-x-1$, where $\varphi$ and $\psi$ are the two canonical ring elements satisfying the golden relation.
background
This module re-derives the T6 golden-ratio forcing node over ℤ[φ] rather than ℝ, so the argument stays inside elementary integer arithmetic and avoids Classical.choice and Real.sqrt. GoldenInt is the structure of pairs $(a,b):\mathbb{Z}\times\mathbb{Z}$ representing $a+b\varphi$, with multiplication folded through the relation $\varphi^{2}=\varphi+1$.
The elements $\varphi$ and $\psi$ are encoded as fixed ring constants (component pairs). Arithmetic is exposed by rfl component lemmas: mul_a, mul_b give the folded product formulas, and the corresponding subtraction and unit lemmas give the integer coordinates of $x-\varphi$, $x-\psi$, and $1$. The local setting is the sigma0 (choice-free) half of the Delta Forcing Spectrum program: factorization first, continuum display later.
proof idea
GoldenInt equality is componentwise, so the proof begins with ext. On each of the two integer coordinates it rewrites with simp only over the component lemmas for subtraction, multiplication, and the constants $\varphi$, $\psi$, and $1$. Each resulting identity in $\mathbb{Z}$ is closed by ring. No quadratic formula, no square roots, and no full simp (banned here for choice contamination).
why it matters
This identity is the algebraic step inside golden_roots: if $x^{2}=x+1$, rewrite via the factorization to obtain $(x-\varphi)(x-\psi)=0$, then split by the integral-domain law to conclude $x=\varphi$ or $x=\psi$. That uniqueness is the choice-free re-derivation of T6 (phi forced as the self-similar fixed point) inside the DeltaSpine program, matching the module verdict target sigma0 DELTA_FORCED. The continuum identification with the real golden ratio is deferred to GoldenIntReal; the factorization itself never leaves ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.