module module high

`IndisputableMonolith.MusicTheory.Consonance`

This module defines consonance for musical intervals by mapping frequency ratios to the J-cost function from Recognition Science. Researchers extending the framework to acoustics or harmonic analysis would cite these definitions when quantifying interval hierarchy. The module is purely definitional, introducing intervalCost, IsConsonant, and explicit evaluations for unison through octave without any theorems or proofs.

claimThe module defines $\mathrm{intervalCost}(r) = J(r)$ for frequency ratio $r > 0$, where $J$ is the Recognition Science cost, together with the predicate $\mathrm{IsConsonant}(r)$ and explicit values such as $\mathrm{intervalCost}(1) = 0$, $\mathrm{intervalCost}(3/2)$ for the fifth, and similar for minor third, major third, fourth, and tritone.

background

The module sits inside the MusicTheory domain and imports the Cost module (which supplies the J-cost) and HarmonicModes (which supplies the underlying interval ratios). It therefore operates in the setting where the Recognition Composition Law and the J-uniqueness $J(x) = (x + x^{-1})/2 - 1$ are already available. Sibling declarations supply concrete evaluations that instantiate the general cost on the standard just intervals.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the interface that lets Recognition Science cost be applied to musical intervals, thereby extending the J-function beyond the core forcing chain (T5) into acoustics. No downstream theorems are listed, so its role is preparatory for any later work that would embed consonance inside the phi-ladder or the eight-tick octave.

scope and limits

Does not prove any theorems relating consonance to physical constants.
Does not introduce or use the phi-ladder or mass formula.
Does not define a numerical threshold for the IsConsonant predicate.
Does not connect interval costs to the Berry creation threshold or Z_cf.

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