extended_ratio_cost_hierarchy
plain-language theorem explainer
The theorem establishes the strict chain of J-cost inequalities across the unison, minor third, major third, fourth, tritone, fifth, and octave. Music theorists working in Recognition Science would cite it to anchor consonance orderings in the multiplicative cost function. The proof is a direct term that packages six already-proved pairwise hierarchy lemmas.
Claim. $J(1) < J(r_{m3}) < J(r_{M3}) < J(r_4) < J(r_{tr}) < J(r_5) < J(2)$, where $J$ is the cost function induced by the multiplicative recognizer on positive ratios and the $r$ symbols denote the standard interval ratios.
background
The MusicTheory.Consonance module defines Jcost via the cost function of MultiplicativeRecognizerL4, which applies derivedCost to the comparator on positive reals. This cost rests on the J function satisfying the Recognition Composition Law and the ledger factorization from DAlembert. Standard interval ratios are taken from MusicalScale (majorThird as $2^{4/12}$, octave as 2) and Constants (octave as eight ticks).
proof idea
The proof is a one-line term wrapper that returns the six-tuple of prior lemmas hierarchy_unison_lt_minorThird, hierarchy_minorThird_lt_majorThird, hierarchy_majorThird_lt_fourth, hierarchy_fourth_lt_tritone, hierarchy_tritone_lt_fifth, and hierarchy_fifth_lt_octave.
why it matters
The result completes the extended ratio cost hierarchy inside the consonance module and directly supports the superparticular claim that the J-cost of $(n+1)/n$ equals $1/(2n(n+1))$. It places musical interval ordering inside the T5 J-uniqueness and T7 eight-tick octave of the forcing chain. No downstream uses appear yet, so its role in larger harmony or scale theorems remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.