module module

`IndisputableMonolith.MusicTheory.Consonance`

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 (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.MusicTheory.HarmonicModes module_import

declarations in this module (23)

def intervalCost L31
theorem intervalCost_eq_jcost L33
def IsConsonant L37
theorem jcost_unison L46
theorem jcost_minorThird L48
theorem jcost_majorThird L49
theorem jcost_fourth L50
theorem jcost_tritone L51
theorem jcost_fifth L52
theorem jcost_octave L53
theorem hierarchy_unison_lt_minorThird L55
theorem hierarchy_minorThird_lt_majorThird L59
theorem hierarchy_majorThird_lt_fourth L63
theorem hierarchy_fourth_lt_fifth L67
theorem hierarchy_fourth_lt_tritone L71
theorem hierarchy_tritone_lt_fifth L75
theorem hierarchy_fifth_lt_octave L79
theorem consonance_hierarchy L83
theorem extended_ratio_cost_hierarchy L95
theorem superparticular_jcost L114
theorem superparticular_jcost_decreasing L122
theorem consonance_is_jcost L141
theorem dissonance_is_high_jcost L146