hierarchy_fourth_lt_fifth
plain-language theorem explainer
The J-cost of the musical fourth interval is strictly less than the J-cost of the fifth interval. Researchers constructing the consonance ordering within Recognition Science music theory cite this link in the chain. The proof is a one-line wrapper that rewrites to the explicit costs 1/24 and 1/12 then applies numerical comparison.
Claim. $Jcost(4/3) < Jcost(3/2)$
background
In the MusicTheory.Consonance module, Jcost assigns recognition costs to intervals and coincides with intervalCost. The fourth and fifth intervals are defined in HarmonicModes as the ratios 4/3 and 3/2. Upstream results fix Jcost fourth at 1/24 and Jcost fifth at 1/12, using the ratio definitions from HarmonicModes and the 3/2 bridge from CircleOfFifths.
proof idea
This is a one-line wrapper proof. It rewrites the goal using jcost_fourth and jcost_fifth to substitute the values 1/24 and 1/12, then invokes norm_num to confirm the inequality.
why it matters
The result is invoked inside consonance_hierarchy to complete the chain of increasing J-costs across unison, minor third, major third, fourth, fifth, and octave. It supplies one concrete step in the Recognition Science derivation of musical consonance from the J-function, consistent with the eight-tick octave. The parent theorem consonance_hierarchy assembles these interval comparisons into the full ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.