fib_0
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 in Recognition Science
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.
scope and limits
- Does not prove any recurrence step beyond the zero case.
- Does not derive the numerical value 45 or the triangular number T(9).
- Does not reference the eight-tick octave or spatial dimension D.
- Does not apply to other initial conditions or shifted Fibonacci sequences.
formal statement (Lean)
54@[simp] lemma fib_0 : fib 0 = 1 := rfl