hierarchy_tritone_lt_fifth
plain-language theorem explainer
The theorem establishes that the J-cost of the tritone interval is strictly less than the J-cost of the perfect fifth. Music theorists applying the Recognition Science cost model to interval hierarchies would cite this result when ordering just-intonation intervals. The proof is a one-line wrapper that substitutes the explicit J-cost values for each interval and reduces the rational comparison by normalization.
Claim. The J-cost of the tritone ratio $45/32$ is strictly less than the J-cost of the perfect fifth ratio $3/2$.
background
In the Consonance module, intervals are assigned J-costs derived from the Recognition Composition Law applied to their frequency ratios. The tritone is defined as the superparticular ratio $45/32$ and the fifth as $3/2$, following the HarmonicModes definitions. Upstream results supply the explicit values: J-cost of the tritone equals $169/2880$ and J-cost of the fifth equals $1/12$. These arise from the J-function in the context of the eight-tick octave.
proof idea
This is a one-line wrapper proof. It rewrites the goal using the theorems supplying the explicit J-cost values for the tritone and the fifth, then applies norm_num to confirm the resulting rational inequality holds.
why it matters
This inequality is invoked by the extended_ratio_cost_hierarchy theorem, which chains cost comparisons from unison through the fifth. It supports the RS-native ordering of musical intervals consistent with the Recognition Composition Law and the phi-ladder structure. The result reinforces the framework claim that lower J-cost correlates with greater consonance inside the D=3 spatial setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.