fibonacci_6_is_8
plain-language theorem explainer
The theorem confirms that the fifth term in the module's Fibonacci sequence equals 8. Researchers deriving the 45-gap from the eight-tick octave and Fibonacci factors cite this to anchor the factorization 45 = 9 × 5. The proof reduces immediately to reflexivity on the recursive definition of the sequence.
Claim. $F_5 = 8$, where the sequence satisfies $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 emerges from the eight-tick structure (T8) combined with the Fibonacci sequence tied to φ. The key factorization is 45 = (8 + 1) × 5, where 9 is the closure factor (one full eight-tick cycle plus return) and 5 is the Fibonacci factor. The local setting uses the triangular number T(9) = 45 to represent cumulative phase accumulation over a closed 8-tick cycle, with lcm(8, 45) = 360 forcing D = 3 spatial dimensions. The fib definition is the standard recurrence starting at 1, 1.
proof idea
The proof is a one-line term that applies reflexivity to the recursive unfolding of fib 5, which computes directly to 8.
why it matters
This computation supports the key result that 45 is not arbitrary but derived from the eight-tick period forced by T8, the closure principle, and cumulative phase. It feeds the parent claim in the same module that 45 = T(9) and combines with the phi-ladder to constrain spatial dimensions. The result touches the open question of how the eight-tick octave (period 2^3) generates the observed constants without additional postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.