fib_pos
plain-language theorem explainer
Fibonacci numbers defined by the standard recursion are strictly positive for every natural number index at least 1. Researchers deriving continued-fraction convergents to the golden ratio cite the result to keep ratios well-defined in recursive relations. The proof runs by induction on the index, dispatching the base case via the hypothesis and applying the recursive definition plus the inductive hypothesis in the successor case.
Claim. For every natural number $n$ satisfying $n ≥ 1$, the Fibonacci number $F_n$ obeys $F_n > 0$.
background
The ContinuedFractionPhi module treats the Fibonacci sequence as the numerators and denominators of the convergents to the infinite continued fraction for φ. The sequence obeys the usual recursion $F_0 = 0$, $F_1 = 1$, $F_{k+2} = F_{k+1} + F_k$, imported from the Gap45 derivation. Positivity guarantees that the ratios $F_{n+1}/F_n$ stay positive and can enter the continued-fraction recursion without division by zero. The module sits inside the larger setting where φ arises as the unique positive fixed point of the map $x ↦ 1 + 1/x$ that minimizes the J-cost functional.
proof idea
The proof is by induction on n. The zero case is discharged immediately by the hypothesis 1 ≤ n via omega. In the successor case the proof splits on the predecessor: the subcase predecessor zero reduces to the definition fib 1 = 1 and is settled by simp; the remaining subcase invokes the inductive hypothesis to obtain positivity of fib (k+1) and finishes with omega on the recursive sum.
why it matters
The lemma is invoked by fibRatio_recursion, which shows that consecutive Fibonacci ratios satisfy the continued-fraction recursion $F_{n+2}/F_{n+1} = 1 + 1/(F_{n+1}/F_n)$. Within Recognition Science it supplies the positivity needed to identify the Fibonacci ratios with the convergents that converge to the self-similar fixed point φ (T6) under sequential J-cost minimization. The result therefore closes one link between the arithmetic ladder and the ground-state geodesic of the J-functional on the positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.