psi_sq
plain-language theorem explainer
In the golden integer ring ℤ[φ], the conjugate root ψ = 1 − φ satisfies the same quadratic ψ² = ψ + 1 that defines φ. Anyone citing the choice-free T6 re-derivation or working with Galois conjugates on the delta spine needs this identity. The proof is a one-line `decide` on the integer components of the ring product.
Claim. In the ring $\mathbb{Z}[\varphi]$ with $\varphi^2 = \varphi + 1$, the conjugate $\psi = 1 - \varphi$ satisfies $\psi \cdot \psi = \psi + 1$.
background
The module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi] \cong \mathbb{Z} \times \mathbb{Z}$, with pairs $(a,b)$ standing for $a + b\varphi$ and multiplication folded through $\varphi^2 = \varphi + 1$. The goal is a sigma0 (choice-free) derivation: only {propext, Quot.sound}, no continuum and no Classical.choice.
Here $\psi$ is the ring element $\langle 1, -1 \rangle$, i.e. $1 - \varphi$, the algebraic conjugate of $\varphi = \langle 0, 1 \rangle$. The same quadratic $x^2 = x + 1$ is the defining relation of the golden ratio in the classical real spine (PhiForcing) and in the real conjugate used by RSSelectionExample. This lemma records that the conjugate still obeys that equation inside the integer ring, before any bridge to $\mathbb{R}$.
proof idea
One-line computational proof: by decide. Both sides expand in components under the GoldenInt multiplication rule
$(a_1 + b_1\varphi)(a_2 + b_2\varphi) = (a_1 a_2 + b_1 b_2) + (a_1 b_2 + b_1 a_2 + b_1 b_2)\varphi$
with $\psi = (1,-1)$. The resulting integer equalities are decidable, so decide closes the goal with no lemmas beyond the ring instances.
why it matters
T6 in the forcing chain forces $\varphi$ as the unique positive self-similar fixed point of the golden equation. This module re-derives that content over $\mathbb{Z}[\varphi]$ so the axiom closure stays sigma0 DELTA_FORCED. Recording that the conjugate $\psi$ also solves $x^2 = x + 1$ is the integer-ring counterpart of the classical fact used on the real spine and in RSSelectionExample.
No downstream theorems currently cite this declaration in the graph, but it sits with the other elementary GoldenInt arithmetic identities (component lemmas, positivity trichotomy, norm) that underwrite the choice-free uniqueness and positivity arguments for $\varphi$. The continuum bridge is deferred to GoldenIntReal, paid once at the display boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.