phi_equation
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1. Researchers deriving the self-similar fixed point in Recognition Science cite this identity when closing the forcing chain from J-uniqueness to the phi-ladder. The proof unfolds the explicit definition of φ, invokes the square-root identity for 5, and finishes with ring normalization plus nonlinear arithmetic.
Claim. Let φ = (1 + √5)/2. Then φ² = φ + 1.
background
In the PhiRing algebra layer, φ is introduced as the positive real (1 + √5)/2 that satisfies the quadratic fixed-point relation required by self-similarity. The module imports Cost and CostAlgebra to equip the reals with the J-cost operations used upstream. The immediate predecessor result, recorded in PhiForcing, states that φ satisfies the golden ratio equation φ² = φ + 1 and is invoked verbatim to supply the algebraic identity.
proof idea
The term proof unfolds the definition of φ, asserts Real.sqrt 5 ^ 2 = 5 via Real.sq_sqrt, applies ring_nf to expand the powers, and closes the equality with nlinarith on the resulting polynomial identity.
why it matters
This identity supplies the algebraic content of the phi-forcing principle, which asserts that self-similarity in a discrete J-cost ledger forces φ as the unique positive solution. It is referenced directly by golden_constraint_unique, phi_inv, phi_satisfies, and economic_inevitability, and realizes the transition from T5 J-uniqueness to T6 where phi becomes the self-similar fixed point. The result also anchors the eight-tick octave and the mass-ladder construction that follows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.