module module

`IndisputableMonolith.Masses.CoherenceExponent`

show as: view Lean formalization →

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

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (23)

theorem fib_4_eq L32
theorem fib_5_eq L35
theorem fib_6_eq L38
theorem fib_recurrence_at_6 L43
theorem fibonacci_deficit L47
def D L53
def octave L56
theorem octave_eq_8 L59
theorem D_is_fib_4 L64
theorem octave_is_fib_6 L69
def coherence_exponent L75
theorem coherence_exponent_eq_5 L78
theorem coherence_exponent_is_fib_5 L83
theorem coherence_exponent_from_fibonacci L87
def is_fibonacci L94
theorem D_1_fibonacci_constraint L98
theorem D_2_fails L102
theorem D_3_fibonacci_constraint L105
theorem D_5_fails L109
theorem D_8_fails L112
theorem coherence_exponent_unique L123
def E_coh L133
theorem E_coh_eq L136