Acoustics Music Consonance From Jcost Music Consonance Cert

The consonance certificate

In music theory, consonance is the quality that makes some intervals sound stable and pleasant, while dissonance makes others sound tense. The octave, fifth, and fourth are classically consonant; the tritone is famously dissonant. A long-standing question is whether this ranking can be derived from a deeper principle. The Recognition Science framework proposes one: it defines a cost function, a number that measures how expensive it is for a system to recognize one value in terms of another, and conjectures that musical consonance is the negative of that cost when applied to the ratio of two frequencies.

The declaration MusicConsonanceCert is a machine-checked certificate, a formal object that bundles together three proved facts about that cost function. First, when the two frequencies are equal, the cost is zero. Second, for any two positive frequencies, the cost is never negative. Third, a particular constant called the canonical threshold, defined as the golden ratio minus three halves, is positive. These three facts are proved in the framework's machine-checked library of formal theorems, and the certificate simply collects them into one structure.

What the certificate does not do is establish anything about music. The cost function in this framework is defined as Jcost (m / e), where m and e are just real numbers called measured and expected. Nothing in the definition ties those numbers to actual frequencies, to human perception, or to the physics of sound. The framework itself says so plainly: it proves nothing specific to this subject. The ranking of intervals from unison to tritone appears in the framework's research notes as an intended direction, not as a proved result.

In Recognition Science, the framework models the cost function J(x) = (x + 1/x)/2 - 1, which is proved to be the unique function satisfying five plain conditions. The consonance idea is to apply that cost to a frequency ratio and order intervals by increasing cost. That would put unison first, octave next, then fifth, fourth, major third, and so on down to the tritone. But this ordering is a hypothesis, not a theorem. The certificate proves the cost function has three basic properties; it does not prove that those properties correspond to musical experience.

What the certificate changes is the status of the framework's claim. It shows that the cost function is well-behaved in the minimal sense needed for a consonance ranking to be possible: equal frequencies cost nothing, positive ratios never cost less than nothing, and the threshold that would separate consonant from dissonant is a real positive number. A reader can now see exactly how much of the musical claim is secured, and exactly where the gap remains.

theorem domainCost_at_equilibrium (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (measured expected : ℝ) : ℝ := Jcost (measured / expected)

What this page does not claim

The certificate does not prove that any specific interval is consonant or dissonant. The certificate does not establish that the J-cost ranking matches human perception of consonance. The certificate does not define what measured and expected frequencies are in musical terms.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Acoustics/MusicConsonanceFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: