Information Phi Hierarchy Growth No Alternative Ratio

The no-alternative lemma

A hierarchy, in the framework's sense, is a sequence of positive numbers K(0), K(1), K(2), ... representing the capacities of successive cache levels, each larger than the last. The framework's cost function J assigns a penalty to the ratio between adjacent levels, and a central question is what growth pattern minimizes that total cost. The answer, proved in the machine-checked library of formal theorems, is that any such hierarchy which is both self-similar and obeys the Fibonacci recurrence must grow by the golden ratio φ, approximately 1.618. The declaration no_alternative_ratio is the formal statement of this uniqueness: given a positive constant ratio r and a positive Fibonacci sequence, the ratio r is forced to equal φ.

The proof rests on a classical fact about Fibonacci sequences. If K(n+2) = K(n+1) + K(n) and all terms are positive, then the ratio of successive terms, r_n = K(n+1)/K(n), satisfies the recursion r_{n+1} = 1 + 1/r_n. The unique positive fixed point of this map is φ, because φ = 1 + 1/φ. The framework's theorem fibonacci_ratio_recursion formalizes this recursion, and fibonacci_ratio_fixed_point confirms that φ is its fixed point. The no-alternative lemma then combines these with the constant-ratio assumption to conclude r = φ, leaving no other positive ratio available for a self-similar Fibonacci hierarchy.

The consequence is structural. The theorem phi_hierarchy_is_unique_fixed_point extends the result: not only is the ratio forced to be φ, but the entire sequence is forced to be K(n) = K(0) · φ^n. This means a J-cost-minimizing system that grows by Fibonacci steps cannot choose a different exponential base; it is locked into the golden ratio. The framework then uses this to show that after N levels, the total complexity is at least K(0) · φ^N, an exponential growth bound. The no-alternative lemma is the hinge: it converts a preference for low cost into a specific, unavoidable growth pattern.

What the declaration does not claim is broader. It does not claim that every hierarchy must be Fibonacci, only that if a hierarchy is both Fibonacci and constant-ratio, its ratio is φ. It does not claim that the golden ratio is optimal in any absolute sense; the proof assumes the Fibonacci recurrence as a constraint, and the cost function's role is to select among self-similar options. It also does not claim that real-world cache hierarchies, which face discrete sizes and other constraints, must follow this exact pattern; the theorem is about the idealized mathematical model.

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

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

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

What this page does not claim

The theorem does not claim every hierarchy is Fibonacci; it only constrains those that are. The theorem does not claim φ is optimal in an unconstrained sense, only under the Fibonacci and constant-ratio assumptions. The theorem does not claim real cache hierarchies must follow this exact pattern, as the model is idealized.

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: