cert
plain-language theorem explainer
Packages the three structural facts needed for J-cost musical consonance: domain cost vanishes on equal ratios, is nonnegative for positive frequencies, and the canonical threshold is positive. Anyone citing the RS consonance ranking (unison through tritone by increasing J) uses this bundle. Proof is a structure instance wiring three local lemmas.
Claim. There is a certificate asserting: (i) the musical domain cost satisfies $C(r,r)=0$ for every nonzero real ratio $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical consonance threshold is strictly positive.
background
The module ranks musical intervals by Recognition Science J-cost. The cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain. Consonance score is $-J(f_1/f_2)$, so smaller $J$ means more consonant: unison ($J=0$), octave, fifth, fourth, major third, minor third, major second, tritone (largest $J$).
Domain cost specializes $J$ to a pair of positive frequency (or ratio) arguments. Equilibrium means equal arguments, where $J(1)=0$. The canonical threshold is the positive cutoff used to separate consonant from dissonant bands.
MusicConsonanceCert is the structure that packages the three algebraic facts any downstream ranking argument needs: vanishing at equilibrium, nonnegativity, and a positive threshold. Upstream, nonnegativity of recognition cost is the standard $J\ge 0$ fact from ObserverForcing.
proof idea
One-line structure instance. The three fields of MusicConsonanceCert are filled by the local lemmas domainCost_at_equilibrium (cost vanishes when the two arguments agree), domainCost_nonneg (nonnegativity for positive arguments, ultimately from $J$-cost nonnegativity), and canonicalThreshold_pos (strict positivity of the cutoff). No extra tactics or rewriting.
why it matters
Closes the certificate side of the module's structural theorem (0 sorry, 0 axiom): consonance ordered by increasing $J$ on frequency ratios. Without this bundle, downstream ranking statements would re-prove vanishing, nonnegativity, and threshold positivity at each use site.
Sits in the acoustics layer that applies the forced $J$ (T5) and the Recognition Composition Law to interval ratios. It does not itself derive the classical interval order; it certifies the cost axioms that make that order a theorem of $J$. No downstream consumers are wired yet in the graph; the sibling cert_inhabited is the natural next step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.