fibonacci_recurrence
plain-language theorem explainer
The declaration defines the Fibonacci recurrence property for a capacity function K from naturals to reals. Cache hierarchy researchers in the Recognition Science framework cite it when deriving self-similar optimality from J-cost minimization. The definition is introduced directly as the partition rule K(ℓ+2) equals K(ℓ+1) plus K(ℓ), serving as the hypothesis base for ratio-forcing lemmas.
Claim. A function $K : ℕ → ℝ$ satisfies the Fibonacci recurrence when $K(ℓ + 2) = K(ℓ + 1) + K(ℓ)$ for every natural number $ℓ$.
background
The Local Cache module verifies core claims from the Inevitability of Local Minds paper, focusing on how J-cost optimal partitioning produces hierarchical cache structures. The recurrence encodes the condition that each level's capacity equals the sum of the two smaller preceding levels, arising from the paper's §4 derivation under assumptions A1–A3. Upstream results supply the dimensionless bridge ratio K defined as φ to the power 1/2 and the universal forcing self-reference structure that supplies the meta-realization axioms.
proof idea
This is a direct definition of the recurrence relation. No lemmas are applied; the body simply states the universal quantification over ℓ of the two-step addition equality.
why it matters
The definition supplies the central hypothesis for the φ-optimal hierarchy theorem and the no-alternative-ratio lemma, both of which conclude that any positive constant-ratio sequence obeying the recurrence must equal φ. It feeds the phiHierarchy_fibonacci theorem and the unique-fixed-point result, closing the loop from J-cost optimality to the self-similar fixed point in the T6 forcing step. The property also appears in the eight-tick periodicity certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.