fibonacci_factor_is_fib
plain-language theorem explainer
The equality confirms that the Fibonacci factor of 5 used in the Gap45 derivation matches the fourth term of the module's recursively defined Fibonacci sequence. Researchers tracing how 45 factors as closure times Fibonacci component in the eight-tick structure would cite this when verifying the algebraic origin of the gap. The proof reduces to a single reflexivity step that aligns the constant definition with the sequence evaluation at index 4.
Claim. $5 = F_4$ where the sequence satisfies $F_0 = 1$, $F_1 = 1$, and $F_{n+2} = F_n + F_{n+1}$ for $n$ a natural number.
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 Fibonacci sequence is defined by fib(0) = 1, fib(1) = 1, fib(n+2) = fib(n) + fib(n+1). The Fibonacci factor is introduced as the constant 5, identified as the smallest Fibonacci number greater than 1 that is coprime with 8, and noted to equal Fib(5) or Fib(4) under the module's indexing.
proof idea
The proof is a one-line reflexivity step that directly equates the constant definition of the Fibonacci factor to the recursive sequence evaluated at index 4.
why it matters
This equality anchors the factorization 45 = 9 × 5 inside the eight-tick derivation, which the module combines with lcm(8,45) = 360 to force D = 3 spatial dimensions. It supports the claim that 45 emerges from the T8 period and Fibonacci properties rather than appearing as an arbitrary constant. The module links the same factorization to cumulative phase accumulation expressed as the ninth triangular number T(9).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.