IndisputableMonolith.Acoustics.MusicPitchJNDFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Musical Pitch JND from J-Cost (Plan v7 fifty-fourth pass)
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 axiom).
   9
  10The just-noticeable difference (JND) for musical pitch is
  11approximately 5-10 cents (1/20 to 1/10 of a semitone) for
  12trained listeners, and about 1 semitone for untrained.
  13
  14RS prediction: the canonical pitch JND corresponds to the
  15recognition quantum J(φ) ≈ 0.118 expressed as a frequency ratio,
  16which gives approximately 10-12 cents (0.10-0.12 semitones).
  17
  18Frequency ratio at J(φ): x such that J(x) = J(φ) = φ - 3/2.
  19Since J is monotone on (1,∞), x = φ ≈ 1.618.
  20But pitch JND is a small ratio near 1; the relevant x is the
  21small-departure approximation: x ≈ 1 + √(2·J(φ)) ≈ 1 + 0.486 → too large.
  22
  23Better: the auditory phi-step is one-eighth of a semitone (8 ticks),
  24giving JND = φ⁻⁸ of the octave ≈ 2^(1/φ⁸) ≈ 2^(0.0081) ≈ 1.0057.
  25That's 5.7 cents — squarely in the trained-listener range.
  26
  27## Falsifier
  28
  29Any psychoacoustic study showing trained-listener pitch JND
  30consistently outside (3, 20) cents.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Acoustics
  35namespace MusicPitchJNDFromJCost
  36
  37open Constants
  38open Cost
  39
  40noncomputable section
  41
  42/-- Pitch JND fraction of the octave: 1/φ⁸. -/
  43def pitchJNDFraction : ℝ := (phi ^ (8 : ℕ))⁻¹
  44
  45theorem pitchJNDFraction_pos : 0 < pitchJNDFraction := by
  46  unfold pitchJNDFraction
  47  apply inv_pos.mpr
  48  apply pow_pos Constants.phi_pos
  49
  50theorem pitchJNDFraction_lt_one : pitchJNDFraction < 1 := by
  51  unfold pitchJNDFraction
  52  rw [inv_lt_one_iff₀]
  53  right
  54  apply one_lt_pow₀ one_lt_phi
  55  norm_num
  56
  57/-- J-cost on the frequency ratio. -/
  58def pitchCost (measured_freq reference_freq : ℝ) : ℝ :=
  59  Jcost (measured_freq / reference_freq)
  60
  61theorem pitchCost_at_unison (f : ℝ) (h : f ≠ 0) :
  62    pitchCost f f = 0 := by
  63  unfold pitchCost; rw [div_self h]; exact Jcost_unit0
  64
  65theorem pitchCost_nonneg (m r : ℝ) (hm : 0 < m) (hr : 0 < r) :
  66    0 ≤ pitchCost m r := by
  67  unfold pitchCost; exact Jcost_nonneg (div_pos hm hr)
  68
  69structure PitchJNDCert where
  70  jnd_pos : 0 < pitchJNDFraction
  71  jnd_lt_one : pitchJNDFraction < 1
  72  cost_at_unison : ∀ f : ℝ, f ≠ 0 → pitchCost f f = 0
  73  cost_nonneg : ∀ m r : ℝ, 0 < m → 0 < r → 0 ≤ pitchCost m r
  74
  75noncomputable def cert : PitchJNDCert where
  76  jnd_pos := pitchJNDFraction_pos
  77  jnd_lt_one := pitchJNDFraction_lt_one
  78  cost_at_unison := pitchCost_at_unison
  79  cost_nonneg := pitchCost_nonneg
  80
  81theorem cert_inhabited : Nonempty PitchJNDCert := ⟨cert⟩
  82
  83end
  84end MusicPitchJNDFromJCost
  85end Acoustics
  86end IndisputableMonolith
  87