theorem
proved
gap_factorization
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
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). -/