hierarchy_fifth_lt_octave
plain-language theorem explainer
The inequality between the J-cost of the perfect fifth ratio and the octave ratio places the fifth strictly below the octave in the recognition ordering. Music theorists extending consonance chains from the J-function would cite this when building the full interval hierarchy. The proof is a one-line wrapper that substitutes the precomputed J-cost values for each ratio and reduces the resulting numerical comparison.
Claim. $Jcost(3/2) < Jcost(2)$
background
The MusicTheory.Consonance module defines J-cost as the recognition cost of a frequency ratio via the J-function from the Cost module. The perfect fifth is the ratio 3/2 and the octave is the ratio 2. Upstream results supply the explicit values: Jcost(3/2) equals 1/12 from the harmonic-modes calculation, while the octave definition ties the ratio 2 to the eight-tick period of the forcing chain.
proof idea
One-line wrapper that rewrites using the explicit J-cost equalities for the fifth and octave ratios, then applies numerical normalization to confirm the strict inequality.
why it matters
This step is invoked by the consonance_hierarchy theorem, which assembles the full chain from unison through fifth to octave, and by the extended_ratio_cost_hierarchy that inserts the tritone. It completes the ordering segment between fourth and octave, aligning with the eight-tick octave period and the 12/8 bridge that identifies the fifth ratio with the semitone count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.