consonance_is_jcost
plain-language theorem explainer
The theorem shows that the cost assigned to a frequency ratio vanishes exactly when that ratio equals one. Music theorists embedding consonance inside the Recognition Science cost framework would cite it to locate perfect unison at the J-equilibrium. The argument is a one-line wrapper that unfolds the intervalCost definition and invokes the general Jcost zero lemma.
Claim. For any real number $r > 0$, the interval cost of ratio $r$ satisfies intervalCost$(r) = 0$ if and only if $r = 1$.
background
In the MusicTheory.Consonance module the function intervalCost is introduced as the direct application of the J-cost to a frequency ratio. The J-cost itself, defined in the Cost module, is the function J(x) = (x + x^{-1})/2 - 1 that quantifies departure from equilibrium. The upstream lemma Jcost_eq_zero_iff from Cost states that J(x) = 0 precisely when x = 1 for positive x; an identical characterization appears in the Navier-Stokes PhiLadderCutoff module.
proof idea
The proof is a one-line wrapper. It unfolds the definition of intervalCost to obtain Jcost r and then applies the lemma Jcost_eq_zero_iff directly to the supplied positive real r.
why it matters
The result places the musical notion of consonance on the same footing as the J-cost equilibrium used throughout the Recognition Science forcing chain. It supplies the zero-cost base case required by the sibling hierarchy theorems that order intervals by increasing J-cost. No downstream uses are recorded yet, but the declaration closes the link between the MusicTheory.Consonance module and the general cost machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.