Information Phi Hierarchy Growth Phi Hierarchy Fibonacci

The Fibonacci recurrence

The Fibonacci recurrence is the rule that each term is the sum of the two before it: K(n+2) = K(n+1) + K(n). The golden ratio phi, about 1.618, is the unique positive number whose square equals itself plus one, phi^2 = phi + 1. Because of that identity, any sequence built by multiplying a starting value by phi at each step, K(n) = K0 * phi^n, automatically satisfies the Fibonacci recurrence. The declaration phiHierarchy_fibonacci establishes exactly this: the framework's canonical phi-geometric sequence, called the phi-hierarchy, obeys the Fibonacci rule at every level.

The proof is a short algebraic check. The sequence at level n+2 is K0 * phi^(n+2). Rewriting phi^2 as phi + 1 turns that into K0 * phi^(n+1) + K0 * phi^n, which is precisely the sum of the two previous levels. The theorem requires only that the starting value K0 is positive, which guarantees every term is positive as well. This is a proved result in the framework's machine-checked library of formal theorems, not a numerical observation.

The same library proves a stronger companion statement: the phi-hierarchy is the unique positive sequence that has both a constant ratio and the Fibonacci recurrence. Any positive sequence with a fixed ratio r that satisfies the recurrence must have r = phi. This uniqueness result, tagged as a theorem, is the "no escape" lemma: there is no alternative constant-ratio Fibonacci sequence. The phi-hierarchy is also the unique fixed point of the ratio map r -> 1 + 1/r, which the Fibonacci recurrence induces on adjacent ratios.

What the declaration does not claim is broader. It does not claim that all Fibonacci sequences grow by phi; the classical Fibonacci numbers 1, 1, 2, 3, 5 have ratios that approach phi but never equal it. It does not claim that any arbitrary hierarchy must be Fibonacci, only that the specific phi-geometric construction satisfies the recurrence. And it does not claim that the phi-hierarchy is the unique solution to any optimization problem by itself; that requires the additional J-cost framework and the uniqueness theorems built around it. The Fibonacci recurrence alone, without the constant-ratio condition, admits many positive sequences.

/-- 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

/-- Any self-similar Fibonacci hierarchy must have ratio φ.
    There is no alternative: any other positive ratio r with Fibonacci
    recurrence is forced to equal φ. This is the "no escape" lemma. -/
theorem no_alternative_ratio (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

/-- **φ-HIERARCHY IS THE UNIQUE FIBONACCI FIXED POINT**

    The phi-hierarchy is the unique positive constant-ratio Fibonacci sequence.
    Any Fibonacci sequence with constant positive ratio must be the phi-hierarchy.
    This is the "gradient flow fixed point" result: the phi-hierarchy cannot be
    improved by any J-cost-preserving Fibonacci-compatible transformation. -/
theorem phi_hierarchy_is_unique_fixed_point (K : ℕ → ℝ) (r : ℝ)
    (hr_pos : 0 < r)
    (hK_pos : ∀ ℓ, 0 < K ℓ)
    (hfib : fibonacci_recurrence K)
    (hratio : constant_ratio K r) :
    r = phi ∧ ∀ n, K n = K 0 * phi ^ n := by
  constructor
  · exact fibonacci_partition_forces_phi K r hr_pos hK_pos hfib hratio
  · intro n
    induction n with
    | zero => simp
    | succ m ih =>
      have := hratio m
      rw [ih] at this
      have hphi_eq := fibonacci_partition_forces_phi K r hr_pos hK_pos hfib hratio
      rw [hphi_eq] at this
      rw [this]
      ring

What this page does not claim

Classical Fibonacci numbers 1, 1, 2, 3, 5 do not have a constant ratio of phi at any finite step. The Fibonacci recurrence alone, without the constant-ratio condition, does not force the golden ratio. The phi-hierarchy is not claimed to be the unique minimum of the J-cost without the full optimization framework.

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: