closure_factor_eq

formal source

  80/-- The closure factor: one full cycle plus return. -/
  81def closure_factor : ℕ := eight_tick_period + 1
  82
  83@[simp] lemma closure_factor_eq : closure_factor = 9 := rfl
  84
  85/-- The Fibonacci factor: smallest Fibonacci > 1 coprime with 8. -/
  86def fibonacci_factor : ℕ := 5
  87
  88@[simp] lemma fibonacci_factor_eq : fibonacci_factor = 5 := rfl
  89
  90/-- 5 is a Fibonacci number. -/
  91theorem fibonacci_factor_is_fib : fibonacci_factor = fib 4 := rfl
  92
  93/-- 5 is coprime with 8. -/
  94theorem fibonacci_factor_coprime_with_8 : Nat.gcd fibonacci_factor 8 = 1 := by
  95  simp [fibonacci_factor]
  96
  97/-! ## The 45-Gap Derivation -/
  98
  99/-- The gap is the product of closure and Fibonacci factors. -/
 100def gap : ℕ := closure_factor * fibonacci_factor
 101
 102/-- **Main Theorem**: The gap equals 45. -/
 103@[simp] theorem gap_eq_45 : gap = 45 := rfl
 104
 105/-- The gap factors as (8+1) × 5. -/
 106theorem gap_factorization : gap = (eight_tick_period + 1) * 5 := rfl
 107
 108/-- The gap is forced by eight-tick and Fibonacci structure. -/
 109theorem gap_forced_from_eight_tick_and_fibonacci :
 110    gap = closure_factor * fibonacci_factor ∧
 111    closure_factor = eight_tick_period + 1 ∧
 112    fibonacci_factor = fib 4 := by
 113  exact ⟨rfl, rfl, rfl⟩