phi_equation
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.
claimLet φ = (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 in Recognition Science
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.
scope and limits
- Does not prove that φ is the unique positive root of the quadratic.
- Does not derive the conjugate equation for ψ or the inverse identity φ⁻¹ = φ - 1.
- Does not connect the equation to J-cost, defectDist, or spatial dimension D = 3.
Lean usage
have h : φ ^ 2 = φ + 1 := phi_equationformal statement (Lean)
80theorem phi_equation : φ ^ 2 = φ + 1 := by
proof body
Term-mode proof.
81 unfold φ
82 have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
83 ring_nf
84 nlinarith [h5]
85
86/-- **THEOREM: ψ² = ψ + 1** (conjugate satisfies the same equation). -/