psi

The module rebuilds the T6 golden-ratio forcing node over the golden ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. Elements are pairs $(a,b)$ standing for $a + b\cdot\varphi$, with multiplication folded through the relation $\varphi^2 = \varphi + 1$. The goal is a sigma0 (choice-free) derivation: ring laws reduce to integer arithmetic, and positivity is a decidable predicate on $(2a+b,b)$, so no continuum or Classical.choice enters the spine.

The conjugate root of $x^2 = x + 1$ is classically $(1-\sqrt{5})/2$. Here it is introduced purely algebraically as $1 - \varphi$. The real display map and the identification with that closed form live in a separate sigma1 bridge module; this definition stays inside elementary $\mathbb{Z}$-arithmetic.

Sibling constants include $\varphi = (0,1)$ and the unit $1 = (1,0)$. Component projections $\psi.a = 1$ and $\psi.b = -1$ are immediate simplifier facts.

Pure definition: the structure constructor packages the pair $(1,-1)$ as an element of GoldenInt. No tactics, no lemmas. Downstream simp lemmas unfold the two components by rfl.

This constant is the second root needed for the choice-free T6 node. It appears in the factorization $(x-\varphi)(x-\psi) = x^2 - x - 1$, which with the integral-domain property yields that the only solutions of $x^2 = x + 1$ in $\mathbb{Z}[\varphi]$ are $\varphi$ and $\psi$. Positivity then singles out $\varphi$, discharging t6_delta_forced without Real.sqrt or Classical.choice.

In the Recognition forcing chain this is the algebraic carrier for T6 (phi forced as the self-similar fixed point). Downstream facts also record $\varphi \neq \psi$ and $\neg\mathrm{IsPos}(\psi)$ (kernel sign check, real value $\approx -0.618$). The continuum tax is paid once at the display boundary, not in this definition.