minorThirdInterval
plain-language theorem explainer
minorThirdInterval packages the ratio 6/5 with its positivity proof into the MusicalInterval structure. Music theorists using Recognition Science would cite it when assembling concrete intervals for J-cost or valence calculations. The definition is a direct constructor application to the pre-defined minorThird value and its norm_num positivity theorem.
Claim. The minor third is the musical interval with ratio $6/5$ satisfying the positivity condition $0 < 6/5$.
background
MusicalInterval is a structure pairing a positive real ratio with a proof of positivity; it also defines a jcost method that applies Jcost to the ratio. The minorThird constant is the real number 6/5, supported by a separate theorem proving positivity via norm_num. This definition appears in the HarmonicModes module, which imports the Cost module to make Jcost available for interval constructions.
proof idea
The definition is a one-line wrapper that applies the MusicalInterval constructor to the minorThird ratio and the minorThird_pos theorem.
why it matters
This definition supplies a concrete minor third for harmonic mode work in the Recognition framework. It draws on the same 6/5 ratio appearing in both HarmonicModes and Valence modules. With no recorded downstream uses, its integration with the phi-ladder or the eight-tick octave remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.