Information Phi Hierarchy Growth Fibonacci Ratio Fixed Point

The Fibonacci ratio fixed point

The golden ratio, usually written φ (phi), is the number that solves r² = r + 1, which is about 1.618. It appears whenever something grows by repeatedly adding its two previous parts, the way Fibonacci numbers do: 1, 1, 2, 3, 5, 8, 13, and so on. In such a sequence, the ratio of one term to the one before it does not stay fixed at the start, but it settles down. The exact statement is a fixed point: if you take any ratio r and feed it into the rule r → 1 + 1/r, the only positive number that comes back unchanged is φ, because φ = 1 + 1/φ.

The framework's machine-checked library of formal theorems proves this fixed point directly. The declaration fibonacci_ratio_fixed_point states that applying the map r ↦ 1 + 1/r to φ yields φ. It is a short, self-contained fact about real numbers, and it does not depend on any framework-specific axioms. The same library also proves the surrounding lemma: in any positive Fibonacci sequence, the ratio of consecutive terms obeys exactly this recursion, rₙ₊₁ = 1 + 1/rₙ. Together these two results pin down why the golden ratio is the only possible long-run ratio for such a sequence.

In Recognition Science, this fixed point is the hinge of a larger argument about growth. The framework models a hierarchy as a sequence of positive levels, and it measures the cost of adjacent levels with a function J. The cost is forced by five plain conditions, and its unique form is J(x) = (x + 1/x)/2 − 1. When a hierarchy must grow, the minimum-cost self-similar solution turns out to be the φ-geometric sequence, where each level is φ times the one before. The library proves that this φ-hierarchy satisfies the Fibonacci recurrence, and that it is the unique positive constant-ratio sequence with that property. The fixed point closes the loop: since the ratio map has only one positive fixed point, there is no other ratio a Fibonacci hierarchy can settle on.

What the declaration does not claim is just as important. It does not say that any actual physical system must follow this rule; that would be a separate empirical claim. It does not prove that the golden ratio is the only fixed point of every ratio map, only of this specific one. And it does not by itself establish the exponential growth result, which is a different theorem in the same file. The fixed point is a precise, narrow fact: the golden ratio is the unique positive solution to r = 1 + 1/r, and the framework uses that fact as a stepping stone, not as a conclusion about the world.

/-- **FIBONACCI RATIO RECURSION**

    In any Fibonacci sequence K(n+2) = K(n+1) + K(n) with positive terms,
    the ratio r_n = K(n+1)/K(n) satisfies r_{n+1} = 1 + 1/r_n.
    The unique positive fixed point of this map is φ (since φ = 1 + 1/φ). -/
theorem fibonacci_ratio_fixed_point :
    (fun r : ℝ => 1 + 1 / r) phi = phi := by
  have hphi_pos : phi ≠ 0 := phi_ne_zero
  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  field_simp
  nlinarith [sq_nonneg phi, phi_pos, hphi_sq]

/-- **FIBONACCI RATIO RECURSION LEMMA**

    If K satisfies Fibonacci recurrence with positive terms,
    the ratio r_{n+1} = 1 + 1/r_n where r_n = K(n+1)/K(n). -/
theorem fibonacci_ratio_recursion (K : ℕ → ℝ)
    (hK_pos : ∀ n, 0 < K n)
    (hfib : fibonacci_recurrence K) (n : ℕ) :
    K (n + 2) / K (n + 1) = 1 + 1 / (K (n + 1) / K n) := by
  have hKn1 : K (n + 1) ≠ 0 := ne_of_gt (hK_pos (n + 1))
  have hKn : K n ≠ 0 := ne_of_gt (hK_pos n)
  have hfib_n := hfib n
  field_simp
  linarith

/-- The φ-hierarchy satisfies the Fibonacci recurrence. -/
theorem phiHierarchy_fibonacci (K₀ : ℝ) (_hK₀ : 0 < K₀) :
    fibonacci_recurrence (phiHierarchy K₀) := by
  intro ℓ
  unfold phiHierarchy
  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  calc K₀ * phi ^ (ℓ + 2)
      = K₀ * (phi ^ ℓ * phi ^ 2) := by ring
    _ = K₀ * (phi ^ ℓ * (phi + 1)) := by rw [hphi_sq]
    _ = K₀ * phi ^ ℓ * phi + K₀ * phi ^ ℓ := by ring
    _ = K₀ * phi ^ (ℓ + 1) + K₀ * phi ^ ℓ := by ring

/-- The φ-hierarchy is the unique constant-ratio hierarchy satisfying Fibonacci. -/
theorem phiHierarchy_unique (K : ℕ → ℝ) (r : ℝ)
    (hr_pos : 0 < r)
    (hK_pos : ∀ ℓ, 0 < K ℓ)
    (hfib : fibonacci_recurrence K)
    (hratio : constant_ratio K r) :
    r = phi := fibonacci_partition_forces_phi K r hr_pos hK_pos hfib hratio

/-- The J-cost of a single adjacent pair in a hierarchy is J(K(ℓ+1)/K(ℓ)). -/
noncomputable def pairCost (K : ℕ → ℝ) (ℓ : ℕ) : ℝ :=
  Jcost (K (ℓ + 1) / K ℓ)

What this page does not claim

It does not claim that any actual physical system must follow the Fibonacci rule. It does not prove that φ is the only fixed point of every ratio map, only of this specific one. It does not by itself establish the exponential growth result, which is a different theorem in the same file.

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/Information/PhiHierarchyGrowth.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: