phi_psi_diff
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.