theorem proved term proof

`fib_6_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  38theorem fib_6_eq : fib 6 = 8 := by native_decide

Term-mode proof.

  39
  40/-! ## The Fibonacci Identity -/
  41
  42/-- The Fibonacci recurrence: F₆ = F₅ + F₄ -/

From the project-wide theorem graph. These declarations reference this one in their body.

fibonacci_deficit in IndisputableMonolith.Masses.CoherenceExponent decl_use
fib_recurrence_at_6 in IndisputableMonolith.Masses.CoherenceExponent decl_use
octave_is_fib_6 in IndisputableMonolith.Masses.CoherenceExponent decl_use

Lean names referenced from this declaration's body.

Identity in IndisputableMonolith.Foundation.LogicAsFunctionalEquation decl_use
fib in IndisputableMonolith.Gap45.Derivation decl_use
fib in IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi decl_use
fib in IndisputableMonolith.Mathematics.RamanujanBridge.ZeckendorfJCost decl_use