phi_psi_diff
plain-language theorem explainer
The difference between the golden ratio φ and its conjugate ψ equals √5. Algebraists manipulating expressions in the phi-ring of Recognition Science would cite this identity for simplifications involving these constants. The proof is a one-line term proof that unfolds the definitions of φ and ψ then applies the ring tactic.
Claim. Let φ = (1 + √5)/2 and ψ = (1 - √5)/2. Then φ − ψ = √5.
background
The declaration sits in Algebra.PhiRing, which defines the phi-ring over the golden ratio and its conjugate. Sibling declarations establish the quadratic equations satisfied by φ and ψ along with their product and sum. The module imports Cost and CostAlgebra, placing the algebra inside the Recognition Science cost framework.
proof idea
One-line term proof: unfold the definitions of φ and ψ, then apply the ring tactic to obtain the identity.
why it matters
This identity supplies a basic algebraic relation used in phi-ring manipulations that feed into Recognition Science derivations of constants and the phi-ladder. It is consistent with the self-similar fixed point φ arising in the T5–T6 steps of the forcing chain. No downstream uses are recorded in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.