module module moderate

`IndisputableMonolith.MusicTheory.HarmonicModes`

HarmonicModes supplies definitions for the octave, fifth, fourth, major and minor thirds, and tritone as superparticular ratios equipped with J-cost properties. Researchers extending Recognition Science to consonance and scale construction cite these when building higher music-theory modules. The module consists of targeted definitions plus elementary comparison lemmas that relate each interval to the superparticular predicate.

claimDefinitions of the octave (ratio $2$), fifth (ratio $3/2$), fourth (ratio $4/3$), major third (ratio $5/4$), minor third (ratio $6/5$), and tritone, each satisfying the superparticular condition $J(r) = (r + r^{-1})/2 - 1$ for integer cost steps.

background

The module belongs to the MusicTheory domain and imports the Cost module to access the J-cost function and Recognition Composition Law. It introduces the superparticular predicate together with named constants for the standard harmonic intervals and lemmas such as octave_eq_superparticular that verify each ratio meets the predicate. These objects instantiate the abstract J-uniqueness at the level of audible frequency ratios.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The interval definitions are imported by CircleOfFifths for scale construction, by Consonance for measuring harmonic relations, and by Valence for affective assignments. They close the step from the abstract RCL and phi-ladder to concrete musical objects, preparing the ground for applications of T5 J-uniqueness inside music theory.

scope and limits

Does not derive the listed ratios from the forcing chain T0-T8.
Does not address microtonal or non-diatonic intervals.
Does not quantify perceptual consonance or valence.
Does not connect intervals to physical constants such as alpha or G.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.MusicTheory.CircleOfFifths module_import
IndisputableMonolith.MusicTheory.Consonance module_import
IndisputableMonolith.MusicTheory.Valence module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (40)

def octave L24
def fifth L25
def fourth L26
def majorThird L27
def minorThird L28
def tritone L29
def superparticular L37
theorem superparticular_pos L40
theorem superparticular_gt_one L47
theorem octave_eq_superparticular L55
theorem fifth_eq_superparticular L59
theorem fourth_eq_superparticular L63
theorem majorThird_eq_superparticular L67
theorem minorThird_eq_superparticular L71
theorem octave_pos L77
theorem fifth_pos L78
theorem fourth_pos L79
theorem majorThird_pos L80
theorem minorThird_pos L81
theorem tritone_pos L82
theorem octave_times_inv L86
theorem fifth_times_fourth_eq_octave L89
theorem octave_is_two L93
structure MusicalInterval L97
def unisonInterval L104
def octaveInterval L107
def fifthInterval L110
def fourthInterval L113
def majorThirdInterval L116
def minorThirdInterval L119
def tritoneInterval L122
theorem unison_jcost L127
theorem octave_jcost L129
theorem fifth_jcost L132
theorem fourth_jcost L135
theorem majorThird_jcost L138
theorem minorThird_jcost L141
theorem tritone_jcost L144
def modesPerOctave L150
theorem modes_from_dimension L152