fibonacci_ratio_forces_golden
A map K from naturals to positive reals obeying both the Fibonacci recurrence and a fixed successive ratio r must satisfy the quadratic r squared equals r plus one. Researchers deriving optimal cache hierarchies or self-similar cost structures cite this lemma as the rigorous core of the phi-optimal hierarchy result. The proof obtains the double-step scaling from the ratio hypothesis, equates it to the additive recurrence, and cancels the positive K term at zero via linear arithmetic.
claimLet $K : ℕ → ℝ$ and $r ∈ ℝ$. Assume $r > 0$, $K(ℓ) > 0$ for every natural $ℓ$, $K(ℓ+2) = K(ℓ+1) + K(ℓ)$ for all $ℓ$, and $K(ℓ+1) = r · K(ℓ)$ for all $ℓ$. Then $r^2 = r + 1$.
background
The Local Cache module supplies the machine-verified core of the Inevitability of Local Minds paper. Its central definitions are the constant-ratio property (each successive level scales by fixed $r$) and the Fibonacci recurrence (additive partition $K_{ℓ+2} = K_{ℓ+1} + K_ℓ$ encoding optimal cost splitting). The module context is cost minimization in hierarchical storage under the Recognition Composition Law and the self-similar fixed point at phi. Upstream, the constant-ratio definition is the universal quantification $K(ℓ+1) = r K(ℓ)$, while the recurrence is the sibling additive rule used to close the quadratic.
proof idea
The tactic proof first applies the constant-ratio hypothesis twice to derive $K(ℓ+2) = r^2 K(ℓ)$. It then substitutes the Fibonacci recurrence and the single-step ratio to obtain $r^2 K(ℓ) = (r + 1) K(ℓ)$ for every $ℓ$. Positivity of $K(0)$ together with nlinarith cancels the common positive factor, yielding the quadratic equation.
why it matters in Recognition Science
This lemma is the direct predecessor of the phi-optimal hierarchy theorem (Theorem 4.2), which upgrades the quadratic to the conclusion $r = phi$. It supplies the rigorous replacement for informal self-similarity arguments inside the Recognition forcing chain, where phi appears as the self-similar fixed point (T6). The result supports downstream claims on working-memory capacity at phi cubed and on the eight-tick octave structure. It touches the open question of whether physical systems realize the exact phi ratio.
scope and limits
- Does not prove existence of any Fibonacci cache hierarchy in physical systems.
- Does not treat time-dependent or non-constant ratios.
- Does not compute explicit cache capacities or access times.
- Does not address non-hierarchical or higher-dimensional storage models.
Lean usage
have h_eq : r ^ 2 = r + 1 := fibonacci_ratio_forces_golden K r hr_pos hK_pos hfib hratioformal statement (Lean)
73theorem fibonacci_ratio_forces_golden (K : ℕ → ℝ) (r : ℝ)
74 (_hr_pos : 0 < r)
75 (hK_pos : ∀ ℓ, 0 < K ℓ)
76 (hfib : fibonacci_recurrence K)
77 (hratio : constant_ratio K r) :
78 r ^ 2 = r + 1 := by
proof body
Tactic-mode proof.
79 -- From constant_ratio: K(ℓ+2) = r * K(ℓ+1) = r * (r * K(ℓ)) = r² * K(ℓ)
80 have hK2 : ∀ ℓ, K (ℓ + 2) = r ^ 2 * K ℓ := by
81 intro ℓ
82 have h1 := hratio (ℓ + 1) -- K(ℓ+2) = r * K(ℓ+1)
83 have h2 := hratio ℓ -- K(ℓ+1) = r * K(ℓ)
84 rw [h2] at h1
85 rw [h1]
86 ring
87 -- From fibonacci_recurrence: K(ℓ+2) = K(ℓ+1) + K(ℓ)
88 -- Combined: r² * K(ℓ) = r * K(ℓ) + K(ℓ) = (r + 1) * K(ℓ)
89 have hcombine : ∀ ℓ, r ^ 2 * K ℓ = (r + 1) * K ℓ := by
90 intro ℓ
91 have h1 := hK2 ℓ
92 have h2 := hfib ℓ
93 have h3 := hratio ℓ
94 linarith
95 -- Since K(0) > 0, we can cancel: r² = r + 1
96 have hK0 := hK_pos 0
97 have h_eq := hcombine 0
98 nlinarith [hK0]
99
100/-- **φ-OPTIMAL HIERARCHY THEOREM (Theorem 4.2, rigorous)**
101
102If a cache hierarchy satisfies:
1031. Fibonacci partition: K_{ℓ+2} = K_{ℓ+1} + K_ℓ (optimal partitioning)
1042. Constant ratio: K_{ℓ+1}/K_ℓ = r (self-similarity)
1053. r > 0, all K_ℓ > 0
106
107Then r = φ = (1+√5)/2. -/