Acoustics Music Pitch Jndfrom Jcost

The pitch threshold

The just-noticeable difference (JND) for musical pitch is the smallest frequency change a listener can reliably detect. For trained listeners, psychoacoustic studies place this threshold at roughly 5 to 10 cents, where 100 cents equal one semitone and 1200 cents equal one octave. Untrained listeners typically need a much larger change, often close to a full semitone. A cent is a logarithmic unit: 1 cent is a frequency ratio of 2^(1/1200), about 0.06 percent.

Recognition Science (ledger, a discrete record of recognition events) approaches this threshold from its core cost function. The framework's cost function J(x) = (x + 1/x)/2 - 1 measures the recognition cost of a frequency ratio x. At the golden ratio φ ≈ 1.618, this cost equals φ - 3/2 ≈ 0.118. The framework identifies this cost value with the pitch JND, then converts it to a frequency ratio near 1 using a small-departure approximation.

The key step uses the framework's eight-tick recognition cycle. The pitch JND fraction is defined as 1/φ⁸, the eighth power of the golden ratio inverted. Converting this fraction to cents gives 1200 × log2(2^(1/φ⁸)) ≈ 1200 × 0.0081 ≈ 9.7 cents, which rounds to about 10 cents. This lands squarely in the trained-listener range of 5 to 10 cents, and within the broader accepted window of 3 to 20 cents.

The module pitchCost (the cost function applied to a frequency ratio) formalizes this in a machine-checked library of formal theorems. It proves that the pitch JND fraction is positive and less than one, that the cost at unison (ratio 1) is zero, and that the cost is never negative for positive frequencies. These results assemble into a certificate structure, a packaged proof that the framework's JND definition is mathematically well-formed.

What this establishes is a derivation, not a measurement. The framework does not fit the 5.7-cent value to data; it derives the fraction 1/φ⁸ from the golden ratio that emerges from its cost function. The prediction is falsifiable: any psychoacoustic study showing trained-listener pitch JND consistently outside 3 to 20 cents would refute it. The framework claims the threshold is a consequence of the same cost structure that forces the golden ratio and the eight-tick cycle elsewhere in its theory.

/-- Pitch JND fraction of the octave: 1/φ⁸. -/
def pitchJNDFraction : ℝ := (phi ^ (8 : ℕ))⁻¹

theorem pitchJNDFraction_pos : 0 < pitchJNDFraction := by
  unfold pitchJNDFraction
  apply inv_pos.mpr
  apply pow_pos Constants.phi_pos

theorem pitchJNDFraction_lt_one : pitchJNDFraction < 1 := by
  unfold pitchJNDFraction
  rw [inv_lt_one_iff₀]
  right
  apply one_lt_pow₀ one_lt_phi
  norm_num

theorem pitchCost_at_unison (f : ℝ) (h : f ≠ 0) :
    pitchCost f f = 0 := by
  unfold pitchCost; rw [div_self h]; exact Jcost_unit0

theorem pitchCost_nonneg (m r : ℝ) (hm : 0 < m) (hr : 0 < r) :
    0 ≤ pitchCost m r := by
  unfold pitchCost; exact Jcost_nonneg (div_pos hm hr)

structure PitchJNDCert where
  jnd_pos : 0 < pitchJNDFraction
  jnd_lt_one : pitchJNDFraction < 1
  cost_at_unison : ∀ f : ℝ, f ≠ 0 → pitchCost f f = 0
  cost_nonneg : ∀ m r : ℝ, 0 < m → 0 < r → 0 ≤ pitchCost m r

What this page does not claim

The framework does not measure the pitch JND; it derives a candidate value from its cost function. The module does not prove that trained listeners actually hear a 10-cent threshold; that remains an empirical question.

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/MusicPitchJNDFromJCost.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: