fibonacci_partition_forces_phi
plain-language theorem explainer
A cache hierarchy obeying the Fibonacci recurrence together with a constant positive ratio r between successive levels must have r equal to the golden ratio phi. Researchers modeling optimal local memory or self-similar information structures in Recognition Science cite this result to derive uniqueness of the phi-hierarchy. The proof first invokes the sibling lemma fibonacci_ratio_forces_golden to reduce the conditions to the quadratic r squared equals r plus one, then uses Constants.phi_sq_eq and nlinarith to identify the unique positive root.
Claim. Let $K : ℕ → ℝ$ be a sequence of positive real numbers satisfying the Fibonacci recurrence $K_{ℓ+2} = K_{ℓ+1} + K_ℓ$ for all $ℓ$ and the constant-ratio condition $K_{ℓ+1}/K_ℓ = r$ with $r > 0$. Then $r = φ$, where $φ = (1 + √5)/2$.
background
The Local Cache module formalizes optimal cache hierarchies whose sizes $K_ℓ$ arise from J-cost symmetry $J(x) = J(1/x)$. Under this symmetry the optimal boundary between levels equates overshoot and undershoot costs, yielding the geometric-mean partition that produces the Fibonacci recurrence $K_{ℓ+2} = K_{ℓ+1} + K_ℓ$. The constant-ratio hypothesis encodes self-similarity of the hierarchy. Upstream, Constants.phi_sq_eq records the identity $φ² = φ + 1$, while the sibling lemma fibonacci_ratio_forces_golden shows that any Fibonacci sequence with constant positive ratio satisfies the same quadratic.
proof idea
The tactic-mode proof begins by applying the sibling lemma fibonacci_ratio_forces_golden to obtain that r satisfies r² − r − 1 = 0. It then invokes Constants.phi_sq_eq to establish that phi satisfies the identical equation. Positivity of r and phi together with nonnegativity of squares are supplied to nlinarith, which concludes that the two positive roots coincide.
why it matters
This is the rigorous statement of the φ-Optimal Hierarchy Theorem (Theorem 4.2). It is invoked directly by phiHierarchy_unique and no_alternative_ratio in PhiHierarchyGrowth, and supports the working-memory-capacity prediction phi³ in localCacheStatus. Within the Recognition framework it realizes the self-similar fixed-point step (T6) for information hierarchies, forcing phi as the unique ratio compatible with Fibonacci partitioning and thereby linking cache structure to the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.