psi_equation
plain-language theorem explainer
The algebraic conjugate ψ of the golden ratio satisfies the same minimal equation ψ² = ψ + 1. Workers on Recognition Science phi-ladder constructions and conjugate identities cite this when closing algebraic relations before mass or forcing derivations. The proof is a direct term-mode reduction: unfold the definition, insert the square-root identity, normalize the ring expression, and finish with nonlinear arithmetic.
Claim. Let ψ denote the algebraic conjugate (1 − √5)/2 of the golden ratio φ. Then ψ² = ψ + 1.
background
In the PhiRing module the golden-ratio conjugate ψ is introduced alongside φ to equip the Recognition algebra with a quadratic ring closed under the same minimal polynomial. The upstream structures supply the J-cost functional J(x) = (x + x⁻¹)/2 − 1 whose fixed-point equation forces φ, and the ledger-factorization context that treats (ℝ₊, ×) as the underlying multiplicative group. The spectral-emergence and complexity-structure imports ensure that the same algebraic relation propagates into discrete tier counts and 8-tick dynamics.
proof idea
The term proof first unfolds the definition of ψ. It then records the elementary identity (√5)² = 5 via Real.sq_sqrt. Ring normalization rewrites the expanded polynomial, after which nlinarith closes the equality using the recorded square identity.
why it matters
The result supplies the conjugate half of the quadratic relation that underpins all subsequent phi-psi identities (product, sum, difference) inside the same module. It directly supports the self-similar fixed-point step (T6) of the unified forcing chain and the phi-ladder mass formula that places physical quantities at integer powers of φ. No downstream theorems yet consume it, leaving the algebraic closure of the ring as an open scaffolding point for later ledger or nucleosynthesis derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.