majorThird
plain-language theorem explainer
The just major third ratio is defined as the real number 5/4. Music theorists and Recognition Science modelers cite this constant when ranking interval consonance via J-cost. The declaration is a direct noncomputable definition equipped with the simp attribute for rewriting.
Claim. The major third interval ratio equals $5/4$.
background
The MusicTheory.Valence module imports HarmonicModes and Mathlib. It defines the major third using the just intonation ratio 5/4, distinct from the equal-tempered version $2^{4/12}$ supplied by Aesthetics.MusicalScale.majorThird. J-cost is the function derived from the Recognition Composition Law that quantifies deviation from unity for interval ratios.
proof idea
The declaration is a one-line definition that directly assigns the value 5/4.
why it matters
This definition supplies the just major third to consonance_hierarchy, extended_ratio_cost_hierarchy, hierarchy_majorThird_lt_fourth and hierarchy_minorThird_lt_majorThird in MusicTheory.Consonance. Those theorems establish the J-cost ordering that feeds the Recognition framework's T5 J-uniqueness step and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.