dissonance_is_high_jcost
plain-language theorem explainer
Any frequency ratio r > 0 with r ≠ 1 yields strictly positive interval cost under the Recognition J-function. Music theorists applying the framework to consonance hierarchies cite this to separate the unison from all other intervals. The proof is a one-line wrapper that unfolds the alias definition of intervalCost and applies the general positivity lemma for Jcost.
Claim. For every real number $r > 0$ with $r ≠ 1$, the interval cost satisfies $0 < J(r)$, where $J$ denotes the J-cost function.
background
The MusicTheory.Consonance module imports the Cost module and defines interval costs for frequency ratios via the J-cost function. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x > 0 and x ≠ 1; its proof rewrites Jcost via the squared form Jcost_eq_sq and applies positivity of squares together with division. intervalCost is introduced as the direct alias noncomputable def intervalCost (r : ℝ) : ℝ := Jcost r, supplying the cost measure used in consonance analysis.
proof idea
The proof is a one-line wrapper. It unfolds the definition of intervalCost to obtain Jcost r, then applies the lemma Jcost_pos_of_ne_one directly to the supplied hypotheses 0 < r and r ≠ 1.
why it matters
The result places all non-unison ratios on the positive side of the J-cost scale, consistent with T5 J-uniqueness in the forcing chain. It supplies the base inequality needed for the sibling hierarchy lemmas that order specific intervals (minor third, tritone, fifth) by increasing J-cost. The declaration therefore anchors the Recognition treatment of musical consonance before any phi-ladder or octave-tick structure is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.