No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
43theorem fib_recurrence_at_6 : fib 6 = fib 5 + fib 4 := by
proof body
Term-mode proof.
44 rw [fib_6_eq, fib_5_eq, fib_4_eq]
45
46/-- Key identity: 8 - 3 = 5, or F₆ - F₄ = F₅ -/
depends on (9)
Lean names referenced from this declaration's body.
-
or
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
fib
in IndisputableMonolith.Gap45.Derivation
decl_use
-
fib_4_eq
in IndisputableMonolith.Masses.CoherenceExponent
decl_use
-
fib_5_eq
in IndisputableMonolith.Masses.CoherenceExponent
decl_use
-
fib_6_eq
in IndisputableMonolith.Masses.CoherenceExponent
decl_use
-
fib
in IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi
decl_use
-
fib
in IndisputableMonolith.Mathematics.RamanujanBridge.ZeckendorfJCost
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use