fibonacci_factor
plain-language theorem explainer
The Fibonacci factor is the constant 5, the smallest Fibonacci number greater than 1 that is coprime to 8. Researchers deriving the 45-gap from the eight-tick structure cite it when factoring gap as closure_factor times this value. The definition is a direct constant assignment with no computation.
Claim. The Fibonacci factor is the natural number $5$.
background
The Gap45 module derives the gap of 45 from the eight-tick period forced by T8 together with the Fibonacci sequence. The eight-tick period equals 8, or 2^3, and the closure factor is defined as 9 to account for return to the initial state after one full cycle. The Fibonacci factor enters as the multiplier that yields gap = 9 * 5 = 45, matching the 9th triangular number T(9) that represents cumulative phase accumulation over the closed cycle.
proof idea
The definition is a direct constant assignment of the value 5. No lemmas or tactics are applied; the body consists solely of the numeral 5.
why it matters
This supplies the Fibonacci component required by the gap definition and the complete derivation D_3_forced_from_structure, which states gap = (eight_tick_period + 1) * fibonacci_factor and concludes D = 3. It fills the factorization step 45 = 9 * 5 that links the eight-tick octave (T8) to the phi-related Fibonacci structure, ensuring coprimality with 8 produces the synchronization period lcm(8,45) = 360.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.