`fib`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.Derivation on GitHub at line 49.

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

  46/-! ## Fibonacci Sequence -/
  47
  48/-- The Fibonacci sequence: 1, 1, 2, 3, 5, 8, 13, 21, ... -/
  49def fib : ℕ → ℕ
  50  | 0 => 1
  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

papers checked against this theorem

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