`gap`

definition

show as: view math explainer →

module: IndisputableMonolith.Gap45.Derivation
domain: Gap45
line: 100 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.Derivation on GitHub at line 100.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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⟩
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.