fibRatio
plain-language theorem explainer
The definition supplies the ratio of consecutive Fibonacci numbers, which serve as convergents to the continued fraction for the golden ratio φ. Analysts of J-cost geodesics and self-similar fixed points cite it when tracing the attractor of the recursion x = 1 + 1/x. The definition is a direct cast of the fib recurrence into real division.
Claim. Let $F_k$ be the Fibonacci sequence with $F_0 = 0$, $F_1 = 1$. For integer $n ≥ 1$, the ratio is $F_{n+1}/F_n$.
background
The module treats continued fractions as sequential J-cost optimizations. The functional J(x) = ½(x + x^{-1}) - 1 has its unique minimum at x = 1 and its self-similar fixed point at φ = (1 + √5)/2. Upstream fib definitions supply the sequence: one version starts at 1,1,2,3,... while the local version starts at 0,1,1,2,... and obeys the recurrence F_{n+2} = F_{n+1} + F_n.
proof idea
This is a one-line definition that casts the integer fib sequence into reals and divides consecutive terms.
why it matters
It supports the fibRatio_recursion theorem that encodes the continued fraction relation F_{n+2}/F_{n+1} = 1 + 1/(F_{n+1}/F_n). The definition fills the link from Fibonacci numbers to the T6 phi fixed point inside the Ramanujan bridge to J-cost geodesics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.