fibonacci_ratio_forces_golden
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.