jcost_fourth
plain-language theorem explainer
The declaration establishes that the J-cost of the musical fourth interval (ratio 4/3) equals exactly 1/24. Researchers constructing consonance hierarchies or interval orderings in Recognition Science would cite this equality to compare recognition costs across common ratios. The proof is a direct one-line wrapper that invokes the matching result already proved in the HarmonicModes module.
Claim. The J-cost of the fourth interval, defined as the ratio 4/3, equals 1/24.
background
The MusicTheory.Consonance module imports Jcost from the Cost module and interval definitions from HarmonicModes. The fourth interval is introduced there as the real number 4/3. The upstream theorem fourth_jcost states that Jcost fourth = 1/24 and proves it by simp [Jcost] followed by ring normalization.
proof idea
This is a one-line wrapper that applies the theorem fourth_jcost from the HarmonicModes module.
why it matters
The result feeds the hierarchy theorems in the same module, including hierarchy_fourth_lt_fifth, hierarchy_fourth_lt_tritone, and hierarchy_majorThird_lt_fourth, each of which rewrites with this equality to obtain a numerical comparison. It supplies one concrete value in the J-cost ordering of intervals that Recognition Science uses to model consonance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.