psi

The ambient module treats the third forcing tag, Selected. The class of ratios obeying the golden constraint $r^2 = r + 1$ without a positivity requirement admits two real roots: the expanding root $\varphi = (1+\sqrt{5})/2$ and its conjugate $\psi = (1-\sqrt{5})/2$. Because both satisfy the same algebraic relation, the bare claim "$r = \varphi$" is not Forced over that class.

In the integer ring $\mathbb{Z}[\varphi]$ the same conjugate appears as the GoldenInt element $\langle 1,-1\rangle$, i.e. $1-\varphi$. The real definition here is the embedding of that algebraic integer into $\mathbb{R}$. The module then shows that adjoining positivity (the physical scale ratio expands, hence $>1$) tightens the class and promotes the claim to Forced.

Pure definition: the body is the classical closed-form expression $(1 - \sqrt{5})/2$. No tactics, no lemmas, no sorry. Noncomputable solely because Real.sqrt is noncomputable in mathlib.

This constant is the witness that "$r = \varphi$" is not Forced over the bare golden class: the conjugate satisfies the same quadratic and differs from $\varphi$. Downstream, GoldenInt uses the algebraic twin to prove golden factorization $(x-\varphi)(x-\psi)=x^2-x-1$, exact roots of the golden equation inside $\mathbb{Z}[\varphi]$, and $\varphi\neq\psi$. Those facts underwrite the module's Selected example and its drainage: positivity tightens the class to the unique expanding root, recovering Forced. In the broader RS chain this is the honest illustration that Selected is an interim tag with an explicit resolution path, not a dumping ground for undecided claims. It sits beside T6 ($\varphi$ as self-similar fixed point) by showing why positivity must be named before $\varphi$ is forced.