Acoustics Music Pitch Jndfrom Jcost Pitch Jndcert

The pitch certificate

The just-noticeable difference (JND) of pitch is the smallest change in frequency that a listener can reliably detect. For trained listeners, psychoacoustic studies place this threshold at roughly 5 to 10 cents, where a cent is one hundredth of a semitone and a semitone is one twelfth of an octave. Untrained listeners need a much larger change, often about a full semitone. The classical fact that trained ears resolve about a tenth of a semitone has been known since the nineteenth century, when experiments on tone discrimination began.

Recognition Science models this threshold with a specific fraction of the octave. The framework's eight-tick recognition cycle divides the octave into eight equal perceptual steps, and the pitch JND is taken to be the size of one such step. That fraction is written as 1/φ⁸, where φ is the golden ratio, approximately 1.618. Since φ⁸ is about 46.98, the fraction is about 1/46.98, which equals a frequency ratio of about 1.0057. In cents, that ratio is about 5.7 cents, squarely inside the trained-listener range. The framework's library of machine-checked formal theorems packages this definition and its basic properties into a structure called PitchJNDCert.

What PitchJNDCert establishes is deliberately narrow. It proves that the fraction 1/φ⁸ is positive and less than one, which is to say the JND is a genuine fraction of the octave, not a zero or a whole octave. It proves that the cost of recognizing a pitch as identical to itself is zero, and that the cost of recognizing any two positive frequencies is never negative. These are structural facts about how the framework assigns a cost to pitch comparison. The certificate does not prove that human ears actually resolve 5.7 cents; that is an empirical claim, checked against psychoacoustic measurements.

The certificate's value is that it pins down a precise prediction. The framework predicts that trained-listener pitch JND should fall in a band from about 3 to 20 cents, with the canonical value near 5.7 cents. The falsifier is named: any study showing trained listeners consistently outside that band would count against the framework. Within the framework, the certificate shows the JND is not a free parameter but a consequence of the same eight-tick cycle that structures other recognition phenomena. What it does not do is claim the measurement itself; that remains a matter for experiment.

/-- 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

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 certificate does not prove that human listeners actually resolve 5.7 cents; that is an empirical measurement. The certificate does not derive the eight-tick cycle from first principles; it assumes that cycle as part of the framework. The certificate does not claim that all listeners, trained or untrained, share the same threshold.

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: