intervalCost_eq_jcost
plain-language theorem explainer
The equality intervalCost r = Jcost r holds identically for every real ratio r. Music theorists applying Recognition Science to consonance would cite this when substituting the J-cost directly into interval calculations. The proof is a one-line reflexivity that follows at once from the definition of intervalCost.
Claim. For every real number $r$, the interval cost equals the J-cost: $intervalCost(r) = Jcost(r)$.
background
The MusicTheory.Consonance module defines intervalCost as a noncomputable wrapper that simply returns Jcost r. Jcost is the Recognition Science cost function satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The present theorem appears immediately after the definition and before the consonance predicate section, making the identification available for hierarchy results on specific intervals.
proof idea
The proof is a term-mode reflexivity that directly invokes the defining equation intervalCost r := Jcost r.
why it matters
This identification embeds musical interval costs inside the J-cost framework that underlies the phi-ladder and the eight-tick octave. It supplies the bridge needed for later consonance predicates to inherit properties from the upstream Cost module without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.