jcost_tritone
plain-language theorem explainer
The theorem supplies the J-cost of the tritone interval ratio 45/32 as the fraction 169/2880. Music theorists applying Recognition Science to just intonation would cite this value when ranking interval dissonance. The proof is a one-line wrapper that directly invokes the precomputed result from the HarmonicModes module.
Claim. The J-cost of the tritone ratio $45/32$ equals $169/2880$.
background
The MusicTheory.Consonance module ranks musical intervals by recognition cost using the J-cost function from the Cost module. The tritone is defined in HarmonicModes as the superparticular ratio 45/32, described as a building block of just intonation with the simplest J-cost. The upstream theorem tritone_jcost states that this cost evaluates to 169/2880 and notes the 8-Tick Connection.
proof idea
This is a one-line wrapper that applies the tritone_jcost lemma from HarmonicModes. That lemma unfolds Jcost on the tritone ratio via simp and confirms the numerical equality with ring.
why it matters
This supplies the numerical value required by the downstream hierarchy theorems that place the tritone between the fourth and fifth in J-cost order. It anchors the consonance comparisons in the MusicTheory.Consonance module and connects to the 8-Tick Connection landmark in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.