fib_6
plain-language theorem explainer
The lemma states that the sixth term in the locally defined Fibonacci sequence equals 13. Workers on the Gap45 derivation cite it to anchor the Fibonacci factor in the factorization of 45 from the eight-tick cycle. The proof is a direct reflexivity reduction after the recursive definition unfolds.
Claim. Let $f : ℕ → ℕ$ satisfy $f(0) = 1$, $f(1) = 1$, and $f(n+2) = f(n) + f(n+1)$ for all $n$. Then $f(6) = 13$.
background
The Gap45.Derivation module proves that 45 emerges from the eight-tick structure (T8) combined with the Fibonacci sequence related to φ. It factors 45 as (8+1) × 5, where 9 is the closure factor for one full cycle plus return and 5 is the Fibonacci factor. The local setting ties this to cumulative phase accumulation as the 9th triangular number T(9) = 45, which with lcm(8,45)=360 forces D=3 spatial dimensions.
proof idea
The proof is a term-mode reflexivity application. It unfolds the local fib definition (0 ↦ 1, 1 ↦ 1, n+2 ↦ fib n + fib (n+1)) to obtain the concrete value 13.
why it matters
This lemma supplies a verified value in the Fibonacci sequence used to factor 45 in the Gap45 derivation. It connects directly to the eight-tick octave (T8) and the phi-related sequence that forces three spatial dimensions via lcm(8,45)=360. The result anchors the numerical ingredients for the module's claim that 45 is not arbitrary but follows from the forcing chain and closure principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.