Acoustics Music Consonance From Jcost Domain Cost At Equilibrium

The equilibrium cost

In the Recognition Science framework, a recognition cost (a number measuring how much work it takes to recognize one thing as another) is assigned to the ratio of two frequencies. The declaration domainCost_at_equilibrium proves a simple, exact fact: when the measured frequency equals the expected frequency, the cost is zero. The proof is one line: it unfolds the definition of the cost and applies a previously established theorem that the cost of recognizing something as itself is zero.

The declaration also establishes two companion facts. First, the cost is never negative when both frequencies are positive, so the cost is a meaningful nonnegative quantity. Second, a threshold value, defined as the golden ratio minus 1.5, is positive. These three facts together form a certificate, a bundle of properties that any candidate consonance ranking must satisfy.

The intended application is a ranking of musical consonance. The idea is to score a pair of frequencies by the cost of recognizing one as the other, then order intervals by increasing cost: unison (cost zero), octave, fifth, fourth, major third, minor third, major second, tritone (largest cost). This ordering matches the traditional consonance ranking of these intervals.

What the declaration does not claim is just as important. The theorem proves nothing specific to music, because the cost function is defined as Jcost (m / e) without any reference to acoustics. It does not prove that the proposed consonance ranking is correct, that the cost function is the only possible one, or that the threshold value has any musical meaning. The code itself states that it proves nothing specific to this subject. The musical interpretation is a research note, not a result.

In Recognition Science, the cost function J is forced by five plain conditions, and this theorem is a small instance of that general theory. The general facts about J, including its vanishing at unity and its nonnegativity, are proved in the framework's machine-checked library of formal theorems. The musical application remains an open hypothesis, not a derived consequence.

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 consonance ranking is not proved correct; it is a research note. The cost function is not shown to be the only possible measure of consonance. The threshold value has no demonstrated musical meaning.

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: