phiHierarchy_fibonacci
plain-language theorem explainer
The sequence K(ℓ) = K₀ φ^ℓ obeys the Fibonacci recurrence K(ℓ+2) = K(ℓ+1) + K(ℓ) for every natural number ℓ whenever the initial scale K₀ is positive. Workers on J-cost minimization for cache hierarchies cite this to verify that the self-similar φ-solution meets the partition constraint forced by optimal boundaries. The proof is a short algebraic reduction that substitutes the identity φ² = φ + 1 and rearranges terms by ring.
Claim. Let K : ℕ → ℝ be given by K(ℓ) = K₀ φ^ℓ. Then K satisfies ∀ ℓ ∈ ℕ, K(ℓ + 2) = K(ℓ + 1) + K(ℓ) whenever K₀ > 0.
background
A hierarchy is a sequence K : ℕ → ℝ of positive real capacities. Its total J-cost is the sum over adjacent levels of J(K(ℓ+1)/K(ℓ)). The module shows that J-cost gradient flow on hierarchies converges to the unique self-similar minimum under the Fibonacci partition constraint. The definition phiHierarchy(K₀) sets K(ℓ) = K₀ · φ^ℓ. The predicate fibonacci_recurrence(K) asserts that every level equals the sum of the two preceding levels: ∀ ℓ, K(ℓ+2) = K(ℓ+1) + K(ℓ). The key algebraic fact used is phi_sq_eq, which states φ² = φ + 1.
proof idea
Unfold the definition of phiHierarchy to obtain K(ℓ) = K₀ φ^ℓ. Apply the identity φ² = φ + 1 to rewrite φ^(ℓ+2) as φ^ℓ · (φ + 1). Distribute and regroup terms to reach K₀ φ^(ℓ+1) + K₀ φ^ℓ, which is exactly the required recurrence. The steps are performed inside a calc block with ring rewrites.
why it matters
This step confirms that the constructed φ-geometric hierarchy satisfies the Fibonacci recurrence required by J-cost optimality. It closes one link in the module argument that gradient descent on hierarchies reaches the φ-partition. The result sits inside the chain that derives exponential growth K₀ · φ^N after N cycles and supports the claim that the φ-ladder is the unique fixed point of the recurrence. It draws on the self-similar fixed-point property of φ from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.