Meta Ledger Uniqueness Phi Satisfies Fixed Point

The fixed point of the golden ratio

The golden ratio, usually written φ, is the number approximately equal to 1.618. It is classically defined as the positive solution to the equation x² = x + 1, which is the same as saying that the ratio of a whole to its larger part equals the ratio of that larger part to the smaller. This definition is framework-neutral and has been known since antiquity, often appearing in geometry and art.

The equation x² = x + 1 has two solutions: one positive and one negative. The positive one is φ = (1 + √5) / 2. The negative solution is approximately -0.618, which is also -1/φ. The positive solution is unique, and this is the content of the theorem named phi_satisfies_fixed_point in the framework's machine-checked library of formal theorems. The library proves that φ² = φ + 1, and it also proves a stronger statement: any positive number x that satisfies x² = x + 1 must equal φ.

The framework calls this a fixed point because the equation can be read as a self-consistency condition. If a cost function J(x) is required to satisfy J(x) = J(1/x), then the point where x = 1/x, which is x = 1, is a trivial fixed point. The nontrivial fixed point of the related equation x² = x + 1 is φ. Within Recognition Science, this uniqueness is used to argue that the golden ratio, not some other number, is the one forced by the framework's axioms. The theorem itself, however, is purely about real numbers and does not depend on any framework-specific assumptions.

What the theorem does not claim is also important. It does not claim that φ is the only solution to the equation in the complex numbers, nor does it claim that the equation x² = x + 1 is the only way to define a fixed point. It also does not claim that the golden ratio is the only self-similar scaling in general; the Cantor set, for example, is self-similar with a scale of 3. The theorem only establishes uniqueness among positive real numbers for this specific equation.

/-- φ is the unique positive solution to x² = x + 1. -/
theorem phi_unique_fixed_point :
    ∀ x : ℝ, x > 0 → x^2 = x + 1 → x = phi := by
  intro x hx hEq
  -- x² = x + 1 ⟹ x² - x - 1 = 0
  have h1 : x^2 - x - 1 = 0 := by linarith

  -- Factorization: x^2 - x - 1 = (x - phi) * (x - psi)
  let psi := (1 - Real.sqrt 5) / 2
  have h_factor : x^2 - x - 1 = (x - phi) * (x - psi) := by
    unfold phi psi
    ring_nf
    rw [Real.sq_sqrt (by norm_num)]
    ring

  rw [h_factor] at h1
  cases mul_eq_zero.mp h1 with
  | inl h => exact sub_eq_zero.mp h
  | inr h =>
    have h_psi_neg : psi < 0 := by
      unfold psi
      have hsqrt : Real.sqrt 5 > 1 := by
        rw [← Real.sqrt_one]
        exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
      linarith
    have h_x_psi : x = psi := sub_eq_zero.mp h
    rw [h_x_psi] at hx
    linarith -- Contradiction: x > 0 but psi < 0

What this page does not claim

The theorem does not claim φ is the only solution over complex numbers. The theorem does not claim the equation x² = x + 1 is the only fixed-point equation of interest. The theorem does not claim the golden ratio is the only self-similar scaling in all contexts.

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/Meta/LedgerUniqueness.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: