fib_0
plain-language theorem explainer
The base case fib(0) = 1 fixes the starting index of the Fibonacci sequence in the Gap45 module. Researchers deriving the 45-gap from eight-tick closure and phi-linked recurrence would invoke it when expanding the product (8+1)×5. The proof is a direct reflexivity match against the defining clause for fib at argument zero.
Claim. $f(0) = 1$, where $f : ℕ → ℕ$ is given by $f(0) = 1$, $f(1) = 1$, and $f(n+2) = f(n) + f(n+1)$ for $n ≥ 0$.
background
The Gap45.Derivation module shows that 45 arises as the product of closure factor 9 (eight ticks plus return) and Fibonacci factor 5. The local fib definition begins 1, 1, 2, 3, 5, … to align indexing with the triangular accumulation T(9) = 45 that represents cumulative phase over a closed eight-tick cycle. Upstream fib declarations in ContinuedFractionPhi and ZeckendorfJCost supply the same recurrence but with different initial indexing; the local version is chosen for direct use in the gap factorization.
proof idea
The proof is a one-line reflexivity step that matches fib 0 against the first clause of the inductive definition of fib.
why it matters
This base case supports the module-level claim that 45 = (8+1)×5 emerges from T8 eight-tick structure combined with the phi-related Fibonacci sequence. It contributes to the argument that lcm(8,45) = 360 forces D = 3 spatial dimensions. No downstream uses appear in the current graph, yet the lemma is required for any unfolding of the recurrence inside the 45-gap derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.