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 introduced as the natural number 5, the smallest Fibonacci number greater than 1 that is coprime to 8. Researchers closing the dimension-forcing argument in Recognition Science cite this constant to produce the 45-tick gap from the eight-tick cycle. The declaration is a direct assignment justified by the surrounding closure and triangular-phase construction.

claimThe Fibonacci factor is the natural number 5, equal to the fourth Fibonacci number in the framework indexing and the smallest such number exceeding 1 while remaining coprime to 8.

background

In the Recognition Science setting the eight-tick period arises directly as 2^3 once spatial dimension is fixed at 3. Closing this cycle requires one additional step, producing a 9-step loop whose cumulative phase equals the ninth triangular number 45. The gap is therefore expressed as the product of this closure factor 9 and the Fibonacci factor 5.

proof idea

The declaration is a one-line definition that directly assigns the value 5. No lemmas or tactics are invoked; the assignment is taken as the numerical factor that satisfies 9 times 5 equals the required gap of 45.

why it matters in Recognition Science

This definition supplies the numerical factor required by the parent theorem D_3_forced_from_structure, which asserts that the eight-tick period equals 8, the gap equals 9 times the Fibonacci factor, and the full period is the least common multiple of 8 and 45. It addresses the paper's noted gap in physical motivation for the 45-tick synchronization by tying the closure principle to the golden-ratio sequence, thereby keeping the T7 eight-tick octave and T8 dimension-forcing steps internally consistent.

scope and limits

formal statement (Lean)

 149def fibonacci_factor : ℕ := 5

proof body

Definition body.

 150
 151/-- 9 × 5 = 45. -/

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.