intervalCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not supply the explicit formula or axioms for Jcost.
- Does not prove positivity or zero-set properties.
- Does not extend to negative or complex ratios.
- Does not define the consonance predicate itself.
formal statement (Lean)
31noncomputable def intervalCost (r : ℝ) : ℝ := Jcost r
proof body
Definition body.
32