`fib_2`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.Derivation on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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
  85/-- The Fibonacci factor: smallest Fibonacci > 1 coprime with 8. -/
  86def fibonacci_factor : ℕ := 5

papers checked against this theorem

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