fibRatio_recursion
plain-language theorem explainer
Fibonacci ratios obey the continued-fraction recurrence: the ratio of consecutive terms equals one plus the reciprocal of the preceding ratio. Analysts of golden-ratio continued fractions or J-cost geodesics cite this identity when deriving the fixed-point property of phi. The proof unfolds the fibRatio definition, invokes the Fibonacci addition identity, and reduces the expression via field simplification and substitution.
Claim. For every natural number $n$ with $n$ at least 2, the ratio of consecutive Fibonacci numbers satisfies $F_{n+1}/F_n = 1 + 1/(F_n/F_{n-1})$, where $F_k$ denotes the $k$-th Fibonacci number.
background
The module treats continued fractions as sequential J-cost optimization on the positive reals. The functional $J(x) = 1/2(x + x^{-1}) - 1$ is strictly convex with unique minimum at $x=1$; its self-similar fixed point is the positive solution of $x = 1 + 1/x$, which is phi. fibRatio n is defined as the real ratio $F_{n+1}/F_n$ and therefore supplies the successive approximants to that fixed point. The present recursion encodes the nesting rule that turns the infinite continued fraction into a Fibonacci recurrence.
proof idea
The tactic proof first obtains auxiliary facts: $n-1$ at least 1, both Fibonacci numbers nonzero via fib_pos, the addition rule $F_{n+1} = F_n + F_{n-1}$ by index arithmetic, and the prior ratio expressed as $F_n/F_{n-1}$. A calc block then rewrites fibRatio n as $F_{n+1}/F_n$, substitutes the addition rule, clears the common term by field_simp, and inverts the ratio to reach the claimed form.
why it matters
The identity supplies the algebraic engine that forces iterated continued-fraction approximants onto phi, the unique positive attractor of the map $x$ maps to $1 + 1/x$. It therefore realizes the self-similar fixed point required after J-uniqueness and directly supports the Hurwitz-optimality claim that phi is the worst approximable irrational. In the Recognition framework this step closes the link between the eight-tick octave, the phi-ladder, and the Ramanujan continued-fraction identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.