module module high

`IndisputableMonolith.Gap45.Derivation`

This module defines the Fibonacci sequence and verifies its initial terms plus selected coprimality properties. Researchers addressing the 45-tick synchronization gap would cite it to supply the combinatorial substrate for cumulative phase counting. The structure consists of a recursive definition followed by direct inductive checks on small indices.

claimThe Fibonacci sequence satisfies $F_1 = 1$, $F_2 = 1$, and $F_n = F_{n-1} + F_{n-2}$ for $n > 2$.

background

The module sits inside the Gap45 subdomain and supplies the number-theoretic objects required to motivate the 45 appearing in the dimension-forcing chain. It introduces the standard Fibonacci sequence beginning 1, 1, 2, 3, 5, 8, 13, 21, … together with its recursive definition on the natural numbers. The setting draws only on basic arithmetic imported from Mathlib; no Recognition Science primitives such as J-cost or the phi-ladder appear here.

proof idea

The module first installs the recursive fib definition. It then proves the explicit values fib 5 = 5 and fib 6 = 8 by direct computation, followed by two coprimality lemmas establishing that consecutive early terms are coprime.

why it matters in Recognition Science

The module feeds the PhysicalMotivation module, which converts the sequence into a cumulative-phase count that grounds the 45-tick synchronization. This step closes the explicit gap noted in the paper for the dimension-forcing argument (T8).

scope and limits

Does not derive a closed-form expression for general terms.
Does not relate the sequence to the J-function or phi fixed point.
Does not contain the 45-tick synchronization argument itself.
Does not import or reference any physics constants.

used by (1)

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

IndisputableMonolith.Gap45.PhysicalMotivation module_import

declarations in this module (38)

def fib L49
lemma fib_0 L54
lemma fib_1 L55
lemma fib_2 L56
lemma fib_3 L57
lemma fib_4 L58
lemma fib_5 L59
lemma fib_6 L60
theorem fibonacci_5_is_5 L63
theorem fibonacci_6_is_8 L66
theorem fib_coprime_4_5 L70
theorem five_eight_coprime L73
def eight_tick_period L78
def closure_factor L81
lemma closure_factor_eq L83
def fibonacci_factor L86
lemma fibonacci_factor_eq L88
theorem fibonacci_factor_is_fib L91
theorem fibonacci_factor_coprime_with_8 L94
def gap L100
theorem gap_eq_45 L103
theorem gap_factorization L106
theorem gap_forced_from_eight_tick_and_fibonacci L109
theorem gap_coprime_with_8 L116
theorem forty_five_eq_nine_times_five L121
theorem forty_five_factorization L124
def full_period L129
theorem full_period_eq_360 L132
theorem full_period_is_product L137
theorem cycles_of_eight L141
theorem cycles_of_gap L145
def power_of_two L151
theorem lcm_360_forces_D_eq_3 L154
theorem D_3_gives_8 L181
theorem D_3_forced_from_structure L184
def closure_interpretation L200
def fibonacci_interpretation L206
def derivation_summary L210