Foundation Universal Forcing Strict Music Ratio Cost

The ratio cost

A frequency ratio is a pair of positive numbers, such as 2/1 for the octave or 3/2 for the perfect fifth. The declaration ratioCost assigns a cost to any two such ratios: 0 when they are equal, 1 when they are not. That is the whole definition. It is a discrete, all-or-nothing ledger: either the ratios match exactly, or they do not, with no middle ground and no graded closeness.

Two elementary properties are proved in the machine-checked library of formal theorems. First, the cost of comparing a ratio to itself is always 0. Second, the cost is symmetric: comparing A to B gives the same result as comparing B to A. These are not assumptions; they are theorems derived from the definition. The definition also fixes the octave as the ratio 2/1 and the perfect fifth as 3/2, familiar musical intervals that serve as concrete examples in the framework's musical realization.

In Recognition Science, this strict cost is the first pass at a musical realization: it treats equality of ratios as the only relevant comparison. The framework's own documentation notes that richer psychoacoustic dissonance costs could refine it later. So ratioCost is a deliberately simple starting point, not a claim about how human ears actually judge intervals. It establishes a minimal, provably symmetric measure of ratio identity, nothing more.

What the declaration does not claim is just as important. It does not claim that equal ratios sound alike, that unequal ratios sound different, or that any particular interval is preferred by listeners. It does not assign a cost to near-misses: 3/2 and 5/4 are both exactly 1 apart, even though one is a perfect fifth and the other a major third. The cost function is a logical scaffold for comparing ratios, not a model of perception.

noncomputable def ratioCost (a b : FrequencyRatio) : Nat :=
  if a = b then 0 else 1

@[simp] theorem ratioCost_self (a : FrequencyRatio) : ratioCost a a = 0 := by
  simp [ratioCost]

theorem ratioCost_symm (a b : FrequencyRatio) : ratioCost a b = ratioCost b a := by
  by_cases h : a = b
  · subst h
    simp [ratioCost]
  · have h' : b ≠ a := by intro hb; exact h hb.symm
    simp [ratioCost, h, h']

def octave : FrequencyRatio := ⟨2, by norm_num⟩

noncomputable def perfectFifth : FrequencyRatio := ⟨(3 : ℝ) / 2, by norm_num⟩

What this page does not claim

It does not claim that equal ratios sound alike or that unequal ratios sound different. It does not assign any graded cost to near-misses such as 3/2 versus 5/4. It does not model human perception of musical intervals.

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/Foundation/UniversalForcing/Strict/Music.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: