minorThird
plain-language theorem explainer
The minor third interval ratio is defined as the real number 6/5. Recognition Science researchers working on interval costs cite this constant when ordering J-cost values in consonance hierarchies. The declaration is a direct noncomputable definition that supplies the just-intonation ratio for downstream calculations without further lemmas.
Claim. The minor third interval ratio is the real number $6/5$.
background
The MusicTheory.Valence module supplies standard frequency ratios for use with the J-cost function imported from HarmonicModes. J-cost measures recognition cost of a ratio x via the function J satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This definition provides the just-intonation value for the minor third, which is then referenced in consonance orderings.
proof idea
The declaration is a direct definition assigning the constant value 6/5. No lemmas or tactics are applied; it functions as a noncomputable abbreviation for the ratio.
why it matters
This definition supplies the minor third ratio to the consonance_hierarchy theorem, which establishes Jcost(1) < Jcost(minorThird) < Jcost(majorThird) < Jcost(fourth) < Jcost(fifth) < Jcost(octave). It anchors the music-theoretic layer of the Recognition framework, feeding the J-uniqueness property (T5) and supporting interval placement within the eight-tick octave (T7). The same definition appears in HarmonicModes to enable related interval mode results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.