theorem
proved
gap_factorization
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gap45.Derivation on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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⟩
114
115/-- 45 is coprime with 8. -/
116theorem gap_coprime_with_8 : Nat.gcd gap 8 = 1 := by
117 simp [gap, closure_factor, fibonacci_factor]
118 decide
119
120/-- Alternative: 45 = 9 × 5. -/
121theorem forty_five_eq_nine_times_five : (45 : ℕ) = 9 * 5 := rfl
122
123/-- 45's prime factorization: 3² × 5. -/
124theorem forty_five_factorization : (45 : ℕ) = 3^2 * 5 := by decide
125
126/-! ## LCM with Eight-Tick -/
127
128/-- The full synchronization period. -/
129def full_period : ℕ := Nat.lcm eight_tick_period gap
130
131/-- **Key Result**: lcm(8, 45) = 360. -/
132@[simp] theorem full_period_eq_360 : full_period = 360 := by
133 simp [full_period, eight_tick_period, gap]
134 decide
135
136/-- 360 = 8 × 45 (since gcd(8, 45) = 1). -/