theorem proved term proof

`fib_5_eq`

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

formal statement (Lean)

  35theorem fib_5_eq : fib 5 = 5 := by native_decide

Term-mode proof.

  36
  37/-- F₆ = 8 (the octave = 2^D) -/

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

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

Lean names referenced from this declaration's body.

octave in IndisputableMonolith.Aesthetics.MusicalScale decl_use
octave in IndisputableMonolith.Constants decl_use
octave in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
fib in IndisputableMonolith.Gap45.Derivation decl_use
octave in IndisputableMonolith.Masses.CoherenceExponent decl_use
fib in IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi decl_use
fib in IndisputableMonolith.Mathematics.RamanujanBridge.ZeckendorfJCost decl_use
octave in IndisputableMonolith.MusicTheory.HarmonicModes decl_use