fib6_eq_2cubeD

formal source

  38theorem fib4_eq_D : Nat.fib 4 = 3 := by decide
  39
  40/-- F(6) = 8 = 2^D = 2^3. -/
  41theorem fib6_eq_2cubeD : Nat.fib 6 = 2 ^ 3 := by decide
  42
  43/-- Recurrence: F(8) = F(7) + F(6) = 13 + 8 = 21. -/
  44theorem fib_recurrence_8 : Nat.fib 8 = Nat.fib 7 + Nat.fib 6 := by decide
  45
  46structure FibonacciCert where
  47  fib3 : Nat.fib 3 = 2
  48  fib4 : Nat.fib 4 = 3
  49  fib6 : Nat.fib 6 = 8
  50  fib6_2cubeD : Nat.fib 6 = 2 ^ 3
  51  recurrence : Nat.fib 8 = Nat.fib 7 + Nat.fib 6
  52
  53def fibonacciCert : FibonacciCert where
  54  fib3 := fib3_eq_2
  55  fib4 := fib4_eq_3
  56  fib6 := fib6_eq_8
  57  fib6_2cubeD := fib6_eq_2cubeD
  58  recurrence := fib_recurrence_8
  59
  60end IndisputableMonolith.Mathematics.FibonacciSequenceFromRS