`fib_0`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gap45.Derivation on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  51  | 1 => 1
  52  | n + 2 => fib n + fib (n + 1)
  53
  54@[simp] lemma fib_0 : fib 0 = 1 := rfl
  55@[simp] lemma fib_1 : fib 1 = 1 := rfl
  56@[simp] lemma fib_2 : fib 2 = 2 := rfl
  57@[simp] lemma fib_3 : fib 3 = 3 := rfl
  58@[simp] lemma fib_4 : fib 4 = 5 := rfl
  59@[simp] lemma fib_5 : fib 5 = 8 := rfl
  60@[simp] lemma fib_6 : fib 6 = 13 := rfl
  61
  62/-- Fibonacci(4) = 5 -/
  63theorem fibonacci_5_is_5 : fib 4 = 5 := rfl
  64
  65/-- Fibonacci(5) = 8 -/
  66theorem fibonacci_6_is_8 : fib 5 = 8 := rfl
  67
  68/-- Consecutive Fibonacci numbers are coprime.
  69    This is a classical result; we prove specific cases by computation. -/
  70theorem fib_coprime_4_5 : Nat.gcd (fib 4) (fib 5) = 1 := by decide
  71
  72/-- 5 and 8 are consecutive Fibonacci numbers, hence coprime. -/
  73theorem five_eight_coprime : Nat.gcd 5 8 = 1 := by decide
  74
  75/-! ## Eight-Tick Structure -/
  76
  77/-- The eight-tick period from T8. -/
  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

papers checked against this theorem

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