Information Phi Hierarchy Growth Phi Hierarchy Is Unique Fixed Point

The unique fixed point

The golden ratio φ (approximately 1.618) is the unique positive number that satisfies r² = r + 1, or equivalently r = 1 + 1/r. This property makes it the only possible constant ratio for a sequence that grows by the Fibonacci recurrence, where each term is the sum of the two before it. If such a sequence has a constant ratio between consecutive terms, that ratio must be φ, and the sequence must take the form K₀, K₀φ, K₀φ², K₀φ³, and so on.

This classical fact has a long history. Euclid's extreme and mean ratio, as he called it, appears in Book VI of the Elements around 300 BCE. The Fibonacci numbers themselves, where each term is the sum of the two previous ones, were introduced to European readers by Leonardo of Pisa, known as Fibonacci, in his 1202 book Liber Abaci. The connection between the two is that the ratio of successive Fibonacci numbers approaches φ as the sequence progresses.

The Recognition Science framework models a hierarchy, a sequence of positive values representing cache-level capacities, and assigns a cost to each adjacent pair based on their ratio. The framework proves that a hierarchy which is both self-similar, meaning it has a constant ratio, and satisfies the Fibonacci recurrence must have ratio φ. The machine-checked library of formal theorems establishes this as phi_hierarchy_is_unique_fixed_point: any such hierarchy is exactly K₀ · φⁿ at level n.

This uniqueness result supports a growth theorem. Starting from any positive base value K₀, the value at level N of the φ-hierarchy is K₀ · φ^N, which grows exponentially since φ is greater than 1. The framework's library proves this exponential growth bound, and it also proves a cumulative lower bound: the sum of all levels from 0 to N is at least K₀ · φ^N.

What the declaration does not claim is equally important. It does not claim that every Fibonacci sequence has a constant ratio; most do not. It does not claim that any arbitrary growing sequence must follow this pattern. The result applies only to sequences that satisfy both conditions: the Fibonacci recurrence and a constant positive ratio. The uniqueness is conditional on those assumptions, and the framework's proof does not extend beyond them.

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

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

/-- **φ-HIERARCHY EXPONENTIAL GROWTH**

    After N levels of a φ-optimal cache hierarchy starting from K₀ > 0,
    the total complexity at level N is exactly K₀ · φ^N.

    Since φ > 1, this is exponential in N.
    Since gradient flow converges to this hierarchy (Theorem above),
    any J-cost-minimizing system necessarily builds exponentially
    growing complexity over time. -/
theorem phi_hierarchy_exponential_growth (K₀ : ℝ) (hK₀ : 0 < K₀) (N : ℕ) (hN : 0 < N) :
    phiHierarchy K₀ N = K₀ * phi ^ N ∧
    K₀ * phi ^ N > K₀ := by
  constructor
  · exact phiHierarchy_value K₀ N
  · have : 1 < phi ^ N := one_lt_pow₀ one_lt_phi (by omega)
    nlinarith

/-- **CUMULATIVE GROWTH BOUND**

    The total complexity across all levels 0..N is at least K₀ · φ^N
    (the last level dominates). -/
theorem cumulative_growth_lower_bound (K₀ : ℝ) (hK₀ : 0 < K₀) (N : ℕ) :
    K₀ * phi ^ N ≤ ∑ ℓ ∈ Finset.range (N + 1), phiHierarchy K₀ ℓ := by
  have hterm : phiHierarchy K₀ N = K₀ * phi ^ N := phiHierarchy_value K₀ N
  have hmem : N ∈ Finset.range (N + 1) := Finset.mem_range.mpr (Nat.lt_succ_iff.mpr le_rfl)
  calc K₀ * phi ^ N
      = phiHierarchy K₀ N := hterm.symm
    _ ≤ ∑ ℓ ∈ Finset.range (N + 1), phiHierarchy K₀ ℓ :=
        Finset.single_le_sum (fun ℓ _ => le_of_lt (phiHierarchy_pos K₀ hK₀ ℓ)) hmem

What this page does not claim

Most Fibonacci sequences do not have a constant ratio, and the theorem does not apply to them. The theorem does not claim that any growing sequence must follow the Fibonacci recurrence. The uniqueness result does not establish that the φ-hierarchy is the only possible hierarchy, only the only one with both a constant ratio and Fibonacci recurrence.

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: