hierarchy_minorThird_lt_majorThird
plain-language theorem explainer
The J-cost of the minor third ratio 6/5 is strictly less than the J-cost of the major third ratio 5/4. Music theorists using Recognition Science to rank interval consonance would cite this to anchor the lower end of the cost hierarchy. The proof is a one-line wrapper that substitutes the explicit cost values 1/60 and 1/40 then normalizes the resulting numerical inequality.
Claim. $J(6/5) < J(5/4)$ where $J(x) = (x + x^{-1})/2 - 1$, with the minor third taken as the ratio 6/5 and the major third as 5/4.
background
The J-cost function is imported from the Cost module and applies the Recognition Science J-function to positive real frequency ratios. In the HarmonicModes module the minor third is defined as the just ratio 6/5 and the major third as 5/4. Upstream theorems supply the concrete values Jcost(6/5) = 1/60 and Jcost(5/4) = 1/40.
proof idea
One-line wrapper that rewrites both sides via the lemmas jcost_minorThird and jcost_majorThird, then applies norm_num to confirm 1/60 < 1/40.
why it matters
The result is invoked inside consonance_hierarchy and extended_ratio_cost_hierarchy to establish the full ascending chain of J-costs from unison through the octave. It instantiates the T5 J-uniqueness step of the forcing chain for musical intervals and closes the corresponding segment of the consonance ordering with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.