fib_1
plain-language theorem explainer
The lemma establishes that the locally defined Fibonacci sequence satisfies its first positive term equals 1. Researchers deriving the 45-gap from eight-tick cycles and phi-linked Fibonacci factors would cite this base case when unfolding terms such as fib(5) for the factorization 45 = 9 * 5. The proof reduces immediately to reflexivity on the second clause of the fib definition.
Claim. The sequence defined by $F_0 = 1$, $F_1 = 1$, and $F_{n+2} = F_n + F_{n+1}$ for $n > 0$ satisfies $F_1 = 1$.
background
The Gap45.Derivation module shows that 45 arises as the product of the closure factor 9 (one full eight-tick cycle plus return) and the Fibonacci factor 5. The fib function is introduced here as the recurrence fib(0) := 1, fib(1) := 1, fib(n+2) := fib(n) + fib(n+1), chosen to align with the triangular-number interpretation T(9) = 45 and the eight-tick structure forced by T8. Upstream fib definitions appear in the RamanujanBridge modules for continued-fraction expansions of phi and for Zeckendorf representations with J-cost, each supplying the same linear recurrence but with differing initial conditions.
proof idea
The proof is a one-line reflexivity wrapper that matches the second defining clause of fib directly.
why it matters
This base case supplies the value fib(5) = 5 required for the factorization 45 = 9 * 5 that links the eight-tick period (T8) to the phi-ladder. It therefore participates in the argument that 45 is not arbitrary but forced by T7 (eight-tick octave), closure, and cumulative phase, which in turn forces D = 3 via lcm(8,45) = 360. The lemma sits inside the chain that connects the Recognition Composition Law and the phi fixed point to concrete numerical gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.