phi_ne_psi
plain-language theorem explainer
In the choice-free golden ring ℤ[φ], the two roots of x² − x − 1 are distinct: φ ≠ ψ. Anyone citing the sigma0 re-derivation of T6 (unique positive golden root without ℝ) needs this separation. The proof is a one-line `decide` on the integer coordinates of the two GoldenInt elements.
Claim. In the ring $\mathbb{Z}[\varphi]$ with elements $(a,b)\mapsto a+b\varphi$, the golden unit $\varphi=(0,1)$ is unequal to its conjugate $\psi=(1,-1)$ (equivalently $\psi=1-\varphi$).
background
This module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]=\mathbb{Z}\times\mathbb{Z}$ rather than over $\mathbb{R}$. Elements are pairs $(a,b)$ read as $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. The goal is a sigma0 (choice-free) derivation: axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$, no Classical.choice.
The two roots of the golden polynomial $x^2-x-1$ appear as ring elements: $\varphi=\langle 0,1\rangle$ and the conjugate $\psi=\langle 1,-1\rangle$, documented as $\psi=1-\varphi$. On the continuum side the same conjugate is $(1-\sqrt{5})/2$; here both live as pure integer pairs, so equality and inequality are decidable componentwise.
The surrounding development encodes positivity via a decidable predicate on $(2a+b,b)$ (sign trichotomy of $s+b\sqrt{5}$ without naming reals), and the integral-domain property via the multiplicative norm $N(a+b\varphi)=a^2+ab-b^2$. Distinctness of the two roots is the elementary first step before uniqueness-of-positive-root arguments.
proof idea
Term-mode proof closed by decide. Both $\varphi$ and $\psi$ are concrete GoldenInt constructors with integer fields $(\varphi_a,\varphi_b)=(0,1)$ and $(\psi_a,\psi_b)=(1,-1)$. Inequality of structures reduces to inequality of $\mathbb{Z}\times\mathbb{Z}$ pairs, which Lean decides by computation. No lemmas beyond the definitions of $\varphi$ and $\psi$ are required.
why it matters
T6 in the forcing chain forces $\varphi$ as the self-similar fixed point of the cost geometry. The classical spine proves that over $\mathbb{R}$ with $\sqrt{5}$ and pays a choice tax; this module re-derives the same content as delta-forced integer arithmetic. Distinct roots are prerequisite to factoring $x^2-x-1=(x-\varphi)(x-\psi)$ inside $\mathbb{Z}[\varphi]$ and to stating that $\varphi$ is the unique positive root without continuum language.
No downstream uses are recorded yet in the graph; the lemma is local infrastructure for the GoldenInt development and for the eventual bridge toReal in GoldenIntReal (where continuum tax is paid once at the display boundary). It supports the Delta Forcing Spectrum program target: every theorem in this file sigma0-auditable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.