module module moderate

`IndisputableMonolith.MusicTheory.Consonance`

The MusicTheory.Consonance module defines interval costs via the J-function and classifies standard musical intervals as consonant or dissonant. Researchers modeling auditory perception within the Recognition Science phi-ladder would cite these definitions when extending J-cost to harmonic ratios. The module supplies explicit J-cost evaluations for unison through octave together with ordering lemmas that establish a consonance hierarchy.

claimThe module introduces the map $Imapsto J(r_I)$ where $r_I$ is the frequency ratio of interval $I$, the predicate IsConsonant$(I)$ holding for low-cost intervals, and explicit values J(unison)=0, J(minor third), J(major third), J(fourth), J(tritone), J(fifth), J(octave) together with the ordering minor third < major third.

background

The module imports the Cost module, which supplies the J-cost function $J(x)=(x+x^{-1})/2-1$ (equivalently cosh(log x)-1) used for recognition defects, and the HarmonicModes module, which defines musical intervals and their rational frequency ratios. In the Recognition Science setting, consonance is the low-J-cost recognition of simple harmonic ratios on the phi-ladder. The module therefore translates the general J-cost into concrete interval costs and introduces the IsConsonant predicate together with comparison lemmas.

proof idea

This is a definition module, no proofs. It consists of the core definitions intervalCost and IsConsonant, followed by direct evaluations of J-cost on the standard intervals and a short chain of ordering lemmas that establish the consonance hierarchy.

why it matters in Recognition Science

The module supplies the concrete consonance definitions required by any downstream application of Recognition Science to music or auditory recognition. It instantiates the J-uniqueness (T5) and phi fixed-point (T6) at musical ratios, providing explicit instances of the Recognition Composition Law for frequency products. No parent theorems are listed in the used-by graph; the definitions stand as the base layer for the music-theory subdomain.

scope and limits

Does not prove any general theorem about arbitrary intervals or non-rational ratios.
Does not connect consonance costs to physical constants alpha, G or hbar.
Does not address microtonal or non-Western tuning systems.
Does not supply a numerical threshold for IsConsonant beyond the listed comparisons.

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