module module

`IndisputableMonolith.MusicTheory.Valence`

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.MusicTheory.HarmonicModes module_import

declarations in this module (19)

def majorThird L28
def minorThird L29
def ledgerSkew L31
theorem ledgerSkew_zero_at_unity L33
theorem ledgerSkew_pos_above_one L36
theorem ledgerSkew_neg_below_one L43
theorem ledgerSkew_antisymmetric L49
theorem major_third_skew L57
theorem minor_third_skew L61
theorem major_third_skew_pos L65
theorem minor_third_skew_pos L70
theorem major_skew_gt_minor_skew L75
inductive Valence L81
def classifyValence L87
theorem major_is_positive L92
theorem minor_is_positive_but_less L98
theorem valence_difference L110
theorem valence_difference_one_twelfth L114
theorem skew_increases_with_interval_size L119