phi_psi_diff
The theorem establishes that the difference between the golden ratio φ and its conjugate ψ equals √5. Researchers deriving algebraic relations for the phi-ladder or J-cost functions in Recognition Science cite this identity as a basic building block. The proof is a direct algebraic reduction obtained by unfolding the definitions of φ and ψ and applying the ring tactic.
claim$φ - ψ = √5$, where φ and ψ are the positive and negative roots of the equation $x^2 - x - 1 = 0$.
background
The PhiRing module supplies the algebraic foundation for Recognition Science by defining φ and ψ as the two real roots of the quadratic $x^2 = x + 1$. These roots appear throughout the cost algebra and the phi-ladder constructions imported from Cost and CostAlgebra. The module also records the companion identities φ + ψ = 1 and φψ = −1, which together fix the scale of all subsequent phi-powers and defect distances.
proof idea
The proof is a one-line term proof. It unfolds the explicit definitions of φ and ψ, then invokes the ring tactic to reduce the difference to √5.
why it matters in Recognition Science
This identity anchors every subsequent manipulation in the PhiRing module and feeds the product and sum theorems that follow it. It supplies the exact numerical gap required by the J-uniqueness relation (T5) and the self-similar fixed-point construction (T6) in the forcing chain. No open scaffolding remains at this step.
scope and limits
- Does not prove the irrationality of φ or ψ.
- Does not supply numerical approximations or bounds.
- Does not extend to higher powers or the phiPow definition.
formal statement (Lean)
105theorem phi_psi_diff : φ - ψ = Real.sqrt 5 := by
proof body
Term-mode proof.
106 unfold φ ψ; ring
107
108/-- **THEOREM: φ⁻¹ = φ − 1** -/