IsConsonant
plain-language theorem explainer
A real ratio r is consonant below threshold t precisely when its J-cost is strictly less than t. Modelers of musical intervals in Recognition Science cite this predicate when ordering intervals by multiplicative strain. It is introduced as a direct abbreviation of the inequality Jcost r < threshold.
Claim. A real ratio $r$ is consonant relative to a threshold $t$ when $J(r) < t$, where $J$ is the J-cost function $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost function quantifies recognition strain for multiplicative ratios and satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). In this module the predicate applies J-cost directly to musical intervals, building on the calibration of J established in LedgerFactorization for the positive reals under multiplication. The supplied comment states that the resulting hierarchy J(1) < J(6/5) < J(5/4) < J(4/3) < J(45/32) < J(3/2) < J(2) is a model-side strain ordering derived purely from the J-cost function.
proof idea
This is a direct definition that sets IsConsonant r threshold to the proposition Jcost r < threshold. No lemmas or tactics are invoked; the declaration functions as an abbreviation for the inequality.
why it matters
The definition supplies the predicate used to state the consonance hierarchy J(1) < J(6/5) < ... < J(2) inside the Recognition Science music-theory layer. It rests on T5 J-uniqueness and the multiplicative structure that later forces the eight-tick octave and D = 3. The module comment explicitly limits its scope to strain ordering rather than a replacement for human music theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.