def
definition
closure_factor
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gap45.Derivation on GitHub at line 81.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
78def eight_tick_period : ℕ := 8
79
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 ∧