Algebra Phi Ring Psi Equation

The companion root

The golden ratio φ = (1+√5)/2 is famous for solving x² = x + 1. Its algebraic conjugate ψ = (1−√5)/2 solves the very same equation. The number ψ is not a new discovery; it is the other root of that quadratic, and it has appeared in mathematics for centuries as the negative reciprocal of φ, since φ·ψ = −1. What the Recognition Science declaration psi_equation establishes is a formal, machine-checked proof that ψ² = ψ + 1, stated as a theorem in the framework's library of formal theorems.

The proof is not a numerical check. It unfolds the definition of ψ, uses the fact that (√5)² = 5, and applies algebraic simplification to verify the identity exactly. The same library also proves the companion facts φ + ψ = 1 and φ − ψ = √5, which together show how the two roots relate. These are not approximations; they are exact identities in the real numbers, derived from the definitions of φ and ψ.

In Recognition Science, the golden ratio is forced by the cost algebra: self-similarity in a discrete ledger requires x² = x + 1, and φ is its unique positive root. The declaration psi_equation does not claim that ψ is forced, nor that it is positive, nor that it plays any role in that forcing argument. It simply records the algebraic fact that ψ obeys the same quadratic equation. The theorem also does not claim that ψ is a unit in the ring ℤ[φ] or that it belongs to that ring at all; ψ is a real number, while the ring ℤ[φ] consists of expressions a + bφ with integers a and b.

What the declaration changes is the reader's picture of the golden ratio's algebraic neighborhood. Knowing that both roots of x² = x + 1 satisfy the same equation, and that they sum to 1 and multiply to −1, gives a complete description of the quadratic field ℚ(√5). The machine-checked proof means this description is not folklore but a verified theorem, ready to be used as a building block for further results in the library.

/-- **THEOREM: ψ² = ψ + 1** (conjugate satisfies the same equation). -/
theorem psi_equation : ψ ^ 2 = ψ + 1 := by
  unfold ψ
  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  ring_nf
  nlinarith [h5]

/-- **THEOREM: φ + ψ = 1** (trace). -/
theorem phi_psi_sum : φ + ψ = 1 := by
  unfold φ ψ; ring

/-- **THEOREM: φ − ψ = √5** -/
theorem phi_psi_diff : φ - ψ = Real.sqrt 5 := by
  unfold φ ψ; ring

/-- **THEOREM: ψ² = ψ + 1** (conjugate satisfies the same equation). -/
theorem psi_equation : ψ ^ 2 = ψ + 1 := by
  unfold ψ
  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  ring_nf
  nlinarith [h5]

What this page does not claim

The declaration does not claim that ψ is positive or that it is the unique positive root of x² = x + 1. The declaration does not claim that ψ is an element of the ring ℤ[φ]. The declaration does not claim that ψ is forced by the cost algebra or plays any role in the forcing argument.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Algebra/PhiRing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: