pith. machine review for the scientific record. sign in
def definition def or abbrev high

fibonacci_factor

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  86def fibonacci_factor : ℕ := 5

proof body

Definition body.

  87

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.