Algebra Phi Ring Phi Psi Product

The golden ratio's partner

The golden ratio φ = (1+√5)/2 is famous for its self-similarity: it is the positive number that satisfies φ² = φ + 1. Less famous is its algebraic conjugate ψ = (1−√5)/2, the other root of the same quadratic equation. The two numbers are bound by three elementary identities: they sum to 1, they differ by √5, and their product is −1. The product identity, φ·ψ = −1, is the one that feels like a small magic trick: two irrational numbers, one positive and one negative, whose product is a plain integer.

The identity is not numerology. It falls out of the defining equation. Since φ and ψ are the two roots of x² = x + 1, their product equals the constant term with a sign, which is −1. This is the standard relationship between roots and coefficients of a quadratic, known since the 16th century work on cubic and quartic equations. The same identity appears in the theory of the Fibonacci numbers, where it underlies identities like Cassini's, and in the arithmetic of the ring Z[φ], the set of all numbers of the form a + bφ with integers a and b.

In Recognition Science, the framework's machine-checked library of formal theorems proves the product identity as the theorem phi_psi_product. The framework models the golden ratio as forced by its cost algebra: self-similarity in a discrete ledger, a record of events, requires x² = x + 1. The theorem states φ·ψ = −1 in the real numbers, and the proof is a direct computation from the definitions of φ and ψ. The library also proves the companion identities φ + ψ = 1 and φ − ψ = √5, and it defines the conjugate map that swaps φ and ψ, showing it preserves multiplication.

What the theorem does not claim is just as important. It does not say that φ·ψ = −1 is a new discovery, nor that it is special to Recognition Science; it is a classical fact about the golden ratio. The theorem does not assert that the product identity holds in the ring Z[φ] itself, only in the real numbers. And it does not claim that the golden ratio is the only number with such a partner; every quadratic irrational has a conjugate. The framework's contribution is not the identity but the proof that it follows from its own axioms, checked line by line by a computer.

The practical payoff is a clean algebraic handle on the golden ratio's arithmetic. The product identity makes φ a unit in its ring: since φ·ψ = −1, multiplying by ψ is the same as dividing by −φ. This is why every power of φ, positive or negative, is again a number of the form a + bφ, and why the ring Z[φ] has the structure of a Euclidean domain, a number system with a division algorithm. The identity is the hinge that lets the whole arithmetic of the golden ratio swing open.

/-- **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** (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** (trace). -/
theorem phi_psi_sum : φ + ψ = 1 := by
  unfold φ ψ; ring

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

/-- **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 product identity is not a new discovery of the framework; it is a classical fact about the golden ratio. The theorem does not assert that φ·ψ = −1 holds inside the ring Z[φ], only in the real numbers. The framework does not claim that the golden ratio is the only number with a conjugate partner.

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: