hierarchy_majorThird_lt_fourth
plain-language theorem explainer
The J-cost of the major third interval is strictly smaller than the J-cost of the perfect fourth. Researchers building the ordering of consonant intervals by recognition cost would cite this step when assembling the full consonance hierarchy. The proof is a one-line wrapper that substitutes the explicit cost values and reduces the resulting numerical comparison.
Claim. The J-cost of the major third satisfies $Jcost(5/4) < Jcost(4/3)$.
background
In the Consonance module the J-cost function assigns a recognition cost to an interval ratio via the J functional of the Recognition framework. The major third is the ratio 5/4 and the perfect fourth is the ratio 4/3. Upstream results supply the concrete values Jcost(5/4) = 1/40 and Jcost(4/3) = 1/24.
proof idea
This is a one-line wrapper. It rewrites the target inequality by the theorems that give the explicit J-cost values for the major third and the fourth, then applies norm_num to confirm the numerical fact 1/40 < 1/24.
why it matters
The lemma supplies the third link in the consonance hierarchy theorem, which states the full chain Jcost(1) < Jcost(minorThird) < Jcost(majorThird) < Jcost(fourth) < Jcost(fifth) < Jcost(octave). It is also used by the extended ratio cost hierarchy. Within Recognition Science the ordering contributes to the derivation of musical consonance from the J functional and the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.