phi_equation
The golden ratio φ obeys φ² = φ + 1. This identity is referenced by arguments that derive φ from self-similarity on a discrete J-cost ledger and by downstream results on forcing principles and economic inevitability. The proof reduces the claim to real arithmetic by unfolding the explicit definition of φ and closing via field simplification with nlinarith on square-root identities.
claimLet $φ = (1 + √5)/2$. Then $φ² = φ + 1$.
background
The PhiForcing module establishes that self-similarity in a discrete ledger equipped with J-cost forces the golden ratio. φ denotes the positive real solution to x² = x + 1, written explicitly as (1 + √5)/2. The upstream Algebra.PhiRing.phi_equation records the identical algebraic identity in a ring setting; the present version re-derives it for direct use in the foundation layer.
proof idea
The tactic sequence unfolds the definition of φ together with squaring, introduces the non-negativity of 5, verifies that the square of its square root recovers 5, applies field simplification, and closes with nlinarith using the square-root identity and non-negativity of squares.
why it matters in Recognition Science
This identity supplies the algebraic core of the phi forcing principle, which states that self-similarity on a J-cost ledger forces the scale ratio to φ. It is invoked directly by golden_constraint_unique, phi_forcing_principle, phi_inv, phi_satisfies, economic_inevitability, and StillnessGenerative results. In the Recognition framework it realizes the T6 step fixing φ as the self-similar fixed point, consistent with the eight-tick octave and D = 3.
scope and limits
- Does not derive the J-cost functional equation or ledger axioms.
- Does not prove uniqueness of φ without the golden constraint hypothesis.
- Does not connect to numerical values of alpha or other RS constants.
- Does not establish existence of self-similar discrete ledgers.
formal statement (Lean)
43theorem phi_equation : φ^2 = φ + 1 := by
proof body
Tactic-mode proof.
44 simp only [φ, sq]
45 have h5 : (0 : ℝ) ≤ 5 := by norm_num
46 have hsq5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
47 field_simp
48 nlinarith [Real.sq_sqrt h5, sq_nonneg (Real.sqrt 5)]
49
50/-- φ is positive. -/