psi_golden
plain-language theorem explainer
The conjugate golden root ψ = (1 − √5)/2 satisfies ψ² = ψ + 1. Anyone auditing the Selected branch of maximal forcing cites this as the admissible counter-model that keeps “r = φ” from being Forced over the golden-only class. The proof is a short real-algebra check: unfold both sides and cancel via √5² = 5.
Claim. The real number $\psi = (1 - \sqrt{5})/2$ satisfies the golden constraint $\psi^2 = \psi + 1$.
background
In Recognition Science, self-similarity of a discrete ledger forces the scale ratio $r$ to obey $r^2 = r + 1$: the next scale equals current plus base (Fibonacci structure). That predicate is the golden constraint. Its two real roots are the expanding root $\varphi = (1+\sqrt{5})/2$ and the contracting conjugate $\psi = (1-\sqrt{5})/2$.
This module sits in Maximal Forcing Phase 4, which exercises the Selected branch honestly. The ambient class is ratios obeying the golden constraint alone, with no positivity cut. Over that class both roots are admissible, so identity with $\varphi$ cannot be Forced until a named selection principle (positivity) tightens the class.
Upstream, the local $\psi$ is the ordinary real conjugate; a sibling GoldenInt encoding $\langle 1,-1\rangle$ records the same algebraic object in the integer lattice $\mathbb{Z}[\varphi]$.
proof idea
Tactic proof. Unfold the golden-constraint predicate and the definition of $\psi$. Record the elementary identity $(\sqrt{5})^2 = 5$ (via Real.sq_sqrt and norm_num). Feed that identity into linear_combination with coefficient $1/4$ to obtain $\psi^2 - \psi - 1 = 0$ after clearing the common denominator $4$. No external lemmas beyond the real square-root API are required.
why it matters
This is the counter-model that makes Selected real rather than decorative. Downstream, isPhi_not_forced_over_Lgolden applies it directly: if “$r=\varphi$” were Forced over the golden-only class, the forcing hypothesis would identify $\psi$ with $\varphi$, contradicting $\psi\neq\varphi$. The same fact supplies the no-model half of the independence witness for the positivity claim and of positiveIndepWitness.
In the framework chain this sits next to T6 (φ forced as the self-similar fixed point): the algebraic constraint alone does not pick the expanding root; positivity (or an equivalent selection) is what promotes the claim from Selected to Forced when the class is tightened from golden-only to positive-golden. The module’s drainage story is exactly that promotion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.