hierarchy_fourth_lt_tritone
plain-language theorem explainer
The inequality between J-costs of the fourth and tritone intervals holds in the Recognition Science ordering. Music theorists extending cost hierarchies for just intonation would cite this link when chaining superparticular ratios. The proof is a one-line wrapper that substitutes the explicit fractional J-cost values and confirms the numerical comparison.
Claim. $J(4/3) < J(45/32)$, where $J$ denotes the J-cost function on positive real ratios.
background
The MusicTheory.Consonance module assigns J-costs to intervals via the J-function imported from the Cost module. The fourth interval is the ratio 4/3 and the tritone is the ratio 45/32, both defined in HarmonicModes as superparticular building blocks. Upstream theorems supply the concrete values J-cost of the fourth equals 1/24 and J-cost of the tritone equals 169/2880.
proof idea
This is a one-line wrapper proof. It rewrites the target using the J-cost equalities for the fourth and tritone, then applies norm_num to compare the resulting fractions.
why it matters
The result supplies the fourth-to-tritone link inside extended_ratio_cost_hierarchy, which assembles the full chain of strict J-cost inequalities across common intervals. It advances the Recognition Science framework by confirming the cost ordering for these superparticular ratios, consistent with the J-uniqueness property and the eight-tick octave structure. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.