phi_psi_product
plain-language theorem explainer
The theorem establishes that the product of the golden ratio φ and its conjugate ψ equals -1. Researchers working on algebraic properties of the phi-ladder in Recognition Science would reference this identity when simplifying expressions involving conjugate pairs. The proof proceeds by direct expansion using the definitions of φ and ψ followed by algebraic simplification and linear arithmetic.
Claim. Let $φ = (1 + √5)/2$ and $ψ = (1 - √5)/2$. Then $φ ψ = -1$.
background
In the PhiRing module, φ and ψ are the two roots of the quadratic x² - x - 1 = 0, with φ the positive golden ratio greater than 1 and ψ its negative conjugate. Sibling results establish the defining equations φ² = φ + 1 and ψ² = ψ + 1 along with positivity and ordering facts. The local algebraic setting supplies the ring operations and normed reals needed for the phi-ladder constructions that later yield constants such as ħ = φ^{-5} and the mass formula on the phi-ladder.
proof idea
The term proof unfolds the explicit definitions of φ and ψ, records the identity (√5)² = 5, applies ring normalization to expand the product, and invokes nonlinear arithmetic on the resulting quadratic expression to obtain -1.
why it matters
This identity is a foundational algebraic relation in the Recognition Science phi-ring. It supports subsequent manipulations of conjugate pairs that appear in the forcing chain (T5 J-uniqueness and T6 self-similar fixed point) and in derivations of the eight-tick octave and D = 3. The result feeds sibling identities such as the sum and difference relations and closes a basic step with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.