phi_psi_sum
plain-language theorem explainer
The sum of the golden ratio φ and its conjugate ψ equals 1. Researchers deriving algebraic identities for the self-similar fixed point or phi-ladder structures would cite this when simplifying paired expressions. The proof is a one-line term wrapper that unfolds the definitions of φ and ψ then applies the ring tactic.
Claim. Let φ = (1 + √5)/2 and ψ = (1 - √5)/2. Then φ + ψ = 1.
background
In the PhiRing module, φ and ψ are the two real roots of the quadratic x² - x - 1 = 0, with φ > 1 serving as the self-similar fixed point and ψ its conjugate. This identity belongs to the basic algebraic toolkit imported from CostAlgebra and used to connect ring operations to the J-cost function. The module establishes these relations before lifting them into the Recognition Science forcing chain.
proof idea
The proof is a term-mode wrapper: unfold φ ψ expands the definitions, after which the ring tactic performs the direct algebraic cancellation to reach 1.
why it matters
This supplies the additive relation between the golden ratio and its conjugate that supports the self-similar fixed point (T6) in the forcing chain. It precedes sibling results such as phi_psi_product and phi_psi_diff, providing the algebraic substrate for phi-ladder mass formulas and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.