majorThird
plain-language theorem explainer
The major third interval ratio is assigned the value 5/4. Music theorists and Recognition Science researchers cite it when ordering intervals by J-cost in consonance hierarchies. The declaration is a direct constant assignment with no further computation or proof steps.
Claim. The major third interval has frequency ratio $5/4$.
background
Recognition Science analyzes musical intervals through the J-cost function, defined via the Recognition Composition Law as $J(x) = (x + x^{-1})/2 - 1$. The HarmonicModes module supplies the basic superparticular ratios used to build harmonic structures and compare consonance. Upstream, the equal-tempered major third is defined as $2^{4/12}$ while the just version matches the valence definition at exactly 5/4.
proof idea
The declaration is a direct definition that assigns the constant value 5/4.
why it matters
This definition supplies the just major third for the consonance hierarchy theorems that establish the J-cost ordering minor third < major third < fourth < fifth < octave. It anchors comparisons in extended ratio cost hierarchies and third quality results that contrast just and equal-tempered tunings. The placement supports the framework's treatment of music intervals as recognition costs on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.