consonance_hierarchy
plain-language theorem explainer
Establishes strict J-cost increase for intervals unison, minor third, major third, fourth, fifth, octave. Recognition Science researchers modeling music perception cite this to derive consonance from the J-function. The proof is a term-mode conjunction of five sub-lemmas.
Claim. J-cost of the unison is strictly less than J-cost of the minor third, which is strictly less than J-cost of the major third, which is strictly less than J-cost of the fourth, which is strictly less than J-cost of the fifth, which is strictly less than J-cost of the octave: $J_{cost}(1) < J_{cost}(r_{minor third}) < J_{cost}(r_{major third}) < J_{cost}(r_{fourth}) < J_{cost}(r_{fifth}) < J_{cost}(r_{octave})$ with standard frequency ratios for each interval.
background
The J-cost function, imported from the Cost module, assigns to each positive real frequency ratio r the value J(r) = (r + r^{-1})/2 - 1. In this module consonance is modeled by ordering intervals according to increasing J-cost. Upstream results supply the concrete ratios: majorThird as 2^{4/12} from MusicalScale, fifth as 3/2 from CircleOfFifths with the doc-comment that the ratio of musical semitones (12) to RS modes (8) is the perfect fifth, and octave as 2 from multiple sources including the eight-tick period.
proof idea
The proof is a term-mode construction that directly assembles the conjunction from five prior hierarchy lemmas. It references hierarchy_unison_lt_minorThird, hierarchy_minorThird_lt_majorThird, hierarchy_majorThird_lt_fourth, hierarchy_fourth_lt_fifth, and hierarchy_fifth_lt_octave with no additional rewriting or case analysis.
why it matters
This theorem completes the consonance ordering inside the MusicTheory.Consonance module and supports applications of the J-function to musical aesthetics. It draws on the octave as the eight-tick period (T7) and the fifth as the 12/8 bridge. The result rests on J-uniqueness (T5) from the forcing chain and provides the ordering needed for interval cost calculations, though it currently has no downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.