golden_roots
plain-language theorem explainer
In the golden ring ℤ[φ], the equation x² = x + 1 has exactly two solutions: φ and its conjugate ψ = 1 − φ. Anyone citing the choice-free T6 node (unique positive self-similar fixed point) needs this root classification. The proof factors the monic golden polynomial and invokes the integral-domain law on ℤ[φ], with no square roots or continuum.
Claim. Let $x$ be an element of the golden ring $\mathbb{Z}[\varphi]$ (integer pairs $(a,b)$ with multiplication folded through $\varphi^2 = \varphi + 1$). If $x^2 = x + 1$, then $x = \varphi$ or $x = \psi$, where $\psi = 1 - \varphi$ is the conjugate root.
background
This module rebuilds the T6 golden-ratio forcing node over the discrete ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. Elements are pairs $(a,b)$ standing for $a + b\varphi$, with the relation $\varphi^2 = \varphi + 1$ baked into the multiplication law, so all ring identities reduce to integer arithmetic.
The conjugate $\psi = \langle 1, -1 \rangle$ satisfies the same monic quadratic. Upstream, golden_factorization states $(x - \varphi)(x - \psi) = x^2 - x - 1$ by componentwise expansion. The ring is an integral domain: mul_eq_zero_iff says a product vanishes iff a factor does, proved via the multiplicative norm $N(a+b\varphi) = a^2 + ab - b^2$ and the irrationality of $\sqrt{5}$ by strong induction on $\mathbb{N}$.
The local goal is sigma0 (axiom closure inside ${\mathrm{propext}, \mathrm{Quot.sound}}$): no Classical.choice, no real square roots in the derivation itself.
proof idea
From the hypothesis $x^2 = x + 1$, rewrite via golden_factorization to obtain $(x - \varphi)(x - \psi) = 0$ after a short ring cleanup. Apply mul_eq_zero_iff to split into $x - \varphi = 0$ or $x - \psi = 0$, then convert each difference to equality. Pure factorization plus the integral-domain law; no quadratic formula and no appeal to $\mathbb{R}$.
why it matters
Feeds directly into t6_delta_forced, the sigma0 packaging of T6: $\varphi$ solves $x^2 = x + 1$, is positive in the decidable integer sign structure, the equation has exactly the roots $\varphi$ and $\psi$, and $\varphi$ is the unique positive root. That theorem is the choice-free counterpart of PhiForcing.phi_unique_self_similar.
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point of the cost geometry. Keeping the root classification inside $\mathbb{Z}[\varphi]$ means the continuum tax is paid only once, at the display bridge in GoldenIntReal, not inside the derivation. This is a concrete step of the Delta Forcing Spectrum program toward a fully sigma0 T6 node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.