intervalCost
plain-language theorem explainer
intervalCost supplies the dissonance measure for any frequency ratio r by direct alias to the J-cost function. Music theorists modeling consonance via Recognition Science cite it to establish that only the unison has zero cost. The definition is a one-line alias to Jcost r.
Claim. For real $r$, the interval cost is defined by $J(r)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
In the MusicTheory.Consonance module the interval cost is introduced after importing the Cost module, which supplies the J-cost function. J-cost quantifies deviation from unity via the Recognition Composition Law and satisfies Jcost_eq_zero_iff for positive r. The local setting treats musical intervals as positive real ratios whose cost is measured on the phi-ladder.
proof idea
One-line definition that aliases intervalCost r to Jcost r.
why it matters
The definition feeds consonance_is_jcost and dissonance_is_high_jcost, which equate zero interval cost with the unison and positive cost with all other intervals. It instantiates the J-uniqueness step (T5) of the forcing chain inside the music-theory domain, allowing consonance to be read off the same cost function used for mass and coupling constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.