psi_equation
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.
claimLet ψ 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 in Recognition Science
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.
scope and limits
- Does not prove that ψ is the unique negative root of the quadratic.
- Does not extend the relation to complex or matrix embeddings.
- Does not derive numerical bounds or approximation rates for ψ.
- Does not connect the equation to explicit physical constants or tiers.
formal statement (Lean)
87theorem psi_equation : ψ ^ 2 = ψ + 1 := by
proof body
Term-mode proof.
88 unfold ψ
89 have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
90 ring_nf
91 nlinarith [h5]
92
93/-- **THEOREM: φ · ψ = −1** (product of conjugates). -/