Algebra Phi Ring Phi Psi Diff

The golden ratio's partner

The golden ratio, usually written φ, is the number (1 + √5)/2, about 1.618. It is the positive solution to the equation x² = x + 1, which means that multiplying by φ is the same as adding 1. Its partner ψ, sometimes called its conjugate, is (1 − √5)/2, about −0.618. The two numbers are the two roots of the same quadratic equation. They are tied together by three simple identities: φ + ψ = 1, φ × ψ = −1, and the one this page is about, φ − ψ = √5.

The difference identity is a small but essential algebraic fact. It says that the gap between the golden ratio and its conjugate is exactly the square root of five, the same √5 that appears in the defining formula. This is not a new discovery; it follows directly from the definitions by elementary algebra. The identity becomes useful when working with the ring ℤ[φ], the set of all numbers of the form a + bφ where a and b are integers. In that ring, the difference φ − ψ is the unit that measures how far a number is from its conjugate, and it appears in the formula for the norm, N(a + bφ) = a² + ab − b².

The identity also plays a role in the Recognition Science framework, which studies a discrete record of events and the forced costs of recognizing them. Within that framework, the golden ratio is not chosen but forced: self-similarity in the ledger requires x² = x + 1, and φ is its unique positive root. The framework's machine-checked library of formal theorems proves φ − ψ = √5 as a lemma, along with the companion identities φ + ψ = 1 and φ × ψ = −1. These are not physical claims; they are algebraic facts about the real numbers, verified by calculation.

What the identity does not do is say anything about the physical world. It does not assert that any measurement of √5 has a particular value, nor that the golden ratio appears in nature. It is a statement about numbers, not about space, time, or matter. The framework's further claims, such as the forcing of physical constants, are separate theorems that build on this algebra but are not contained in it. The difference identity is a tool, not a conclusion.

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

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

/-- **THEOREM: φ · ψ = −1** (product of conjugates). -/
theorem phi_psi_product : φ * ψ = -1 := by
  unfold φ ψ
  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  ring_nf
  nlinarith [h5]

/-- **THEOREM: φ² = φ + 1** (the defining equation). -/
theorem phi_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 identity φ − ψ = √5 does not assert any physical measurement or empirical fact. The identity does not imply that the golden ratio appears in nature or in any physical system. The identity does not by itself force any physical constant or dimension.

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: