fibonacci_ratio_recursion
plain-language theorem explainer
Any positive sequence K obeying the Fibonacci recurrence satisfies the ratio recursion r_{n+1} = 1 + 1/r_n. Researchers deriving self-similar fixed points on the phi-ladder cite it when showing that J-cost descent forces the golden-ratio partition. The proof is a one-line algebraic reduction: positivity rules out zero denominators, the recurrence instance is instantiated, and field_simp plus linarith close the equality.
Claim. Let $K : ℕ → ℝ$ be positive and satisfy the Fibonacci recurrence. Then for every $n ∈ ℕ$, $K(n+2)/K(n+1) = 1 + 1/(K(n+1)/K(n))$.
background
In the J-cost gradient flow setting, a hierarchy is a sequence of positive reals K : ℕ → ℝ giving cache capacities at successive levels. Total cost is the sum of J-ratios between adjacent levels; the Fibonacci recurrence is the relation forced by the Recognition Composition Law at optimal boundaries, so that self-similar growth minimizes cost. The upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost of recognition events, while Constants.K anchors the bridge ratio to phi^{1/2}.
proof idea
Positivity of K yields K(n+1) ≠ 0 and K(n) ≠ 0. The recurrence hypothesis is instantiated at n. Field_simp clears the resulting fractional equation and linarith discharges the linear identity.
why it matters
The lemma supplies the ratio recursion needed to prove that the phi-hierarchy is the unique positive Fibonacci fixed point, as stated in the module doc-comment. It fills the T6 step forcing phi as the self-similar fixed point and supports the claim that J-cost descent on hierarchies converges to the phi partition. It feeds the sibling uniqueness results phiHierarchy_unique and fibonacci_ratio_fixed_point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.