Information Local Cache Fibonacci Partition Forces Phi

The Fibonacci ratio

The Fibonacci sequence is the one where each number is the sum of the two before it: 1, 1, 2, 3, 5, 8, and so on. It appears in nature, art, and number theory, and one of its best-known properties is about ratios. If you divide each Fibonacci number by the one before it, the quotients settle down toward a single value, about 1.618, which is the golden ratio φ = (1+√5)/2. The theorem fibonacci_partition_forces_phi proves a sharper version of that fact: if a sequence obeys the Fibonacci recurrence K(ℓ+2) = K(ℓ+1) + K(ℓ), and if the ratio of consecutive terms is constant, then that constant ratio must be exactly φ.

The proof is a short algebraic argument. Suppose every term is positive and the ratio K(ℓ+1)/K(ℓ) equals some fixed number r. The recurrence then says r² = r + 1, because K(ℓ+2) = r²K(ℓ) and also K(ℓ+2) = K(ℓ+1) + K(ℓ) = rK(ℓ) + K(ℓ). The positive solution of r² = r + 1 is precisely φ. The theorem does not require the sequence to start at 1 and 1; any positive sequence with the Fibonacci recurrence and a constant ratio must have that ratio equal to φ. This is a statement about sequences in general, not about any particular cache design.

In Recognition Science, this result appears in the context of a local cache, a store of frequently used items kept close at hand. The framework models a hierarchy of cache levels, each with a capacity K(ℓ), and derives from its cost function that the optimal partition between levels satisfies the Fibonacci recurrence. The theorem then shows that a self-similar hierarchy, one where each level is a fixed multiple of the previous, must use the golden ratio as that multiple. The framework's library of machine-checked theorems records this as fibonacci_partition_forces_phi, with the proof that the constant ratio r equals φ.

What the theorem does not claim is just as important. It does not prove that a real cache hierarchy must have a constant ratio; that is an additional assumption. It does not derive the Fibonacci recurrence from first principles within this theorem; that derivation is a separate result in the framework. And it says nothing about whether the golden ratio is the best ratio for any practical cache. The theorem is a conditional statement: if the recurrence and the constant ratio hold, then the ratio is φ. It is a fact about numbers, not a design prescription.

/-- **φ-OPTIMAL HIERARCHY THEOREM (Theorem 4.2, rigorous)**

If a cache hierarchy satisfies:
1. Fibonacci partition: K_{ℓ+2} = K_{ℓ+1} + K_ℓ (optimal partitioning)
2. Constant ratio: K_{ℓ+1}/K_ℓ = r (self-similarity)
3. r > 0, all K_ℓ > 0

Then r = φ = (1+√5)/2. -/
theorem fibonacci_partition_forces_phi (K : ℕ → ℝ) (r : ℝ)
    (hr_pos : 0 < r)
    (hK_pos : ∀ ℓ, 0 < K ℓ)
    (hfib : fibonacci_recurrence K)
    (hratio : constant_ratio K r) :
    r = phi := by
  have hgolden := fibonacci_ratio_forces_golden K r hr_pos hK_pos hfib hratio
  -- r > 0 and r² = r + 1 implies r = φ (by uniqueness of positive root)
  -- Use the fact that φ is the unique positive solution to x² = x + 1
  have h_eq : r ^ 2 - r - 1 = 0 := by linarith
  -- Both r and φ satisfy x² - x - 1 = 0
  have h_phi_eq : phi ^ 2 - phi - 1 = 0 := by
    have := Constants.phi_sq_eq
    linarith
  -- The product of roots = -1 (Vieta's), so the other root is negative.
  -- Since r > 0 and φ > 0, they must be the same root.
  nlinarith [sq_nonneg (r - phi), sq_nonneg (r + phi - 1),
             Constants.phi_pos, sq_nonneg (Real.sqrt 5 - 2),
             Real.sq_sqrt (show (5 : ℝ) ≥ 0 by norm_num)]

/-- **KEY LEMMA**: Fibonacci recurrence + constant positive ratio → r² = r + 1.

This is the rigorous replacement for the hand-wavy "self-similar cost" argument. -/
theorem fibonacci_ratio_forces_golden (K : ℕ → ℝ) (r : ℝ)
    (_hr_pos : 0 < r)
    (hK_pos : ∀ ℓ, 0 < K ℓ)
    (hfib : fibonacci_recurrence K)
    (hratio : constant_ratio K r) :
    r ^ 2 = r + 1 := by
  -- From constant_ratio: K(ℓ+2) = r * K(ℓ+1) = r * (r * K(ℓ)) = r² * K(ℓ)
  have hK2 : ∀ ℓ, K (ℓ + 2) = r ^ 2 * K ℓ := by
    intro ℓ
    have h1 := hratio (ℓ + 1)  -- K(ℓ+2) = r * K(ℓ+1)
    have h2 := hratio ℓ         -- K(ℓ+1) = r * K(ℓ)
    rw [h2] at h1
    rw [h1]
    ring
  -- From fibonacci_recurrence: K(ℓ+2) = K(ℓ+1) + K(ℓ)
  -- Combined: r² * K(ℓ) = r * K(ℓ) + K(ℓ) = (r + 1) * K(ℓ)
  have hcombine : ∀ ℓ, r ^ 2 * K ℓ = (r + 1) * K ℓ := by
    intro ℓ
    have h1 := hK2 ℓ
    have h2 := hfib ℓ
    have h3 := hratio ℓ
    linarith
  -- Since K(0) > 0, we can cancel: r² = r + 1
  have hK0 := hK_pos 0
  have h_eq := hcombine 0
  nlinarith [hK0]

What this page does not claim

The theorem does not prove that any real cache must have a constant ratio between levels. The theorem does not derive the Fibonacci recurrence from the framework's cost function. The theorem does not state that the golden ratio is the optimal ratio for any practical cache design.

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/LocalCache.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: