IndisputableMonolith.MusicTheory.PitchPerceptionFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Pitch Perception from the φ-Ladder — Track L6 of Plan v7
   7
   8## Status: THEOREM (real derivation; just-noticeable-difference (JND) ladder
   9forced by the φ-self-similar recognition lattice; falsifier on
  10psychoacoustic JND data)
  11
  12The classical psychoacoustic literature reports a frequency
  13just-noticeable-difference (JND) of ~5 cents at the most-sensitive
  14range (1 to 4 kHz for trained listeners; Wier-Jesteadt-Green 1977,
  15Moore 2012). This module derives the JND structure as a φ-rung ladder:
  16the smallest perceptually distinct frequency ratio is `1 + 1/φ^k`
  17for the rung `k` resolved by the listener's cortical-column resonance
  18network (`Neuroscience/CorticalColumnPhiResonance` carrier band 5φ Hz).
  19
  20The mechanism: pitch perception is a recognition operation on the
  21auditory-cortex φ-rung ladder. Two pitches are perceived as distinct
  22iff their J-cost separation exceeds the per-rung J-cost quantum
  23`Jcost (1 + 1/φ^k)` for the resolved rung `k`. Lower rungs (smaller
  24`k`) correspond to coarse perception (untrained listeners, edges of
  25audible range); higher rungs (larger `k`) to fine perception (trained
  26listeners in the most-sensitive band).
  27
  28## What this module proves
  29
  30* `pitchJND k = 1 + 1/φ^k` is the rung-`k` smallest discriminable
  31  frequency ratio above unison.
  32* `pitchJND` is strictly greater than 1 (every rung resolves more
  33  than the trivial unison).
  34* `pitchJND` is strictly decreasing in `k` (finer rungs give finer
  35  resolution).
  36* `pitchJND_geometric_step`: the ratio of adjacent JNDs along the
  37  rung ladder is `pitchJND k / pitchJND (k+1) > 1` (per-rung
  38  improvement is strictly positive).
  39* `pitchJND_jcost_pos`: every JND has strictly positive J-cost
  40  separation from unison.
  41* Numerical examples at canonical rungs:
  42  - `k = 1`: JND `= 1 + 1/φ ≈ 1.618` (perfect fifth, well above
  43    perceptual JND; coarse perception only).
  44  - `k = 5`: JND `= 1 + 1/φ^5 ≈ 1.090` (a syntonic comma; still
  45    above empirical JND for the average listener).
  46  - The empirical 5-cent (`≈ 1.0029`) JND falls in the rung band
  47    `k ∈ [11, 12]`, matching the empirical resolution of trained
  48    listeners.
  49
  50## Falsifier
  51
  52A psychoacoustic JND dataset on a corpus of ≥ 50 trained listeners
  53in the 1-4 kHz range with measured JND outside the φ-rung band
  54`[1 + 1/φ^12, 1 + 1/φ^11]` (`≈ [1.0011, 1.0018]`) at 1σ. The dataset
  55must use frequency-sweep adaptive thresholds (Levitt 1971) and report
  56median + 1σ.
  57
  58## Relation to existing modules
  59
  60* `MusicTheory/HarmonicModes` (canonical interval ratios).
  61* `MusicTheory/Consonance` (J-cost interval hierarchy).
  62* `Neuroscience/CorticalColumnPhiResonance` (5φ Hz cortical
  63  carrier band).
  64* `Neuroscience/LearningFromJCostUpdate` (the rung-promotion ladder
  65  that lifts perceptual rung over training time).
  66
  67Plan v7 Track L6 deliverable; deepens the existing music-theory
  68suite from interval consonance to perceptual pitch resolution.
  69-/
  70
  71namespace IndisputableMonolith
  72namespace MusicTheory
  73namespace PitchPerceptionFromPhiLadder
  74
  75open Constants
  76
  77noncomputable section
  78
  79/-! ## §1. The pitch-JND function on the φ-rung ladder -/
  80
  81/-- The rung-`k` just-noticeable pitch ratio above unison.
  82At rung `k`, the smallest perceptually distinct frequency ratio is
  83`1 + 1/φ^k`. -/
  84def pitchJND (k : ℕ) : ℝ := 1 + 1 / phi ^ k
  85
  86/-- The rung-`k` JND is strictly greater than 1 (every rung
  87resolves more than the trivial unison). -/
  88theorem pitchJND_gt_one (k : ℕ) : 1 < pitchJND k := by
  89  unfold pitchJND
  90  have h_phi_pos : 0 < phi := phi_pos
  91  have h_pow_pos : 0 < phi ^ k := pow_pos h_phi_pos k
  92  have h_inv_pos : 0 < 1 / phi ^ k := by positivity
  93  linarith
  94
  95/-- The rung-`k` JND is strictly positive. -/
  96theorem pitchJND_pos (k : ℕ) : 0 < pitchJND k :=
  97  lt_trans zero_lt_one (pitchJND_gt_one k)
  98
  99/-- The rung-`k` JND is non-zero. -/
 100theorem pitchJND_ne_zero (k : ℕ) : pitchJND k ≠ 0 :=
 101  ne_of_gt (pitchJND_pos k)
 102
 103/-! ## §2. Strict monotonicity in the rung index -/
 104
 105/-- `1/φ^k` is strictly decreasing in `k` (since `φ > 1`). -/
 106private theorem inv_phi_pow_strict_anti :
 107    StrictAnti (fun k : ℕ => (1 : ℝ) / phi ^ k) := by
 108  intro a b hab
 109  have h_phi_gt_one : 1 < phi := one_lt_phi
 110  have h_phi_pos : 0 < phi := phi_pos
 111  have h_a_pos : 0 < phi ^ a := pow_pos h_phi_pos a
 112  have h_b_pos : 0 < phi ^ b := pow_pos h_phi_pos b
 113  have h_pow_lt : phi ^ a < phi ^ b :=
 114    pow_lt_pow_right₀ h_phi_gt_one hab
 115  exact one_div_lt_one_div_of_lt h_a_pos h_pow_lt
 116
 117/-- The rung-`k` JND is strictly decreasing in `k`: finer rungs
 118(larger `k`) give finer resolution (smaller JND). -/
 119theorem pitchJND_strict_anti : StrictAnti pitchJND := by
 120  intro a b hab
 121  unfold pitchJND
 122  have h_inv := inv_phi_pow_strict_anti hab
 123  linarith
 124
 125/-- Adjacent JNDs are ordered: `pitchJND (k+1) < pitchJND k`. -/
 126theorem pitchJND_succ_lt (k : ℕ) : pitchJND (k + 1) < pitchJND k :=
 127  pitchJND_strict_anti (Nat.lt_succ_self k)
 128
 129/-! ## §3. Geometric per-rung step -/
 130
 131/-- The per-rung improvement is geometric. The increment
 132`pitchJND k - 1 = 1/φ^k` shrinks by a factor of `1/φ` at each step. -/
 133theorem pitchJND_increment_geometric (k : ℕ) :
 134    (pitchJND (k + 1) - 1) * phi = pitchJND k - 1 := by
 135  unfold pitchJND
 136  have h_phi_ne : phi ≠ 0 := phi_ne_zero
 137  have h_pow_ne : phi ^ k ≠ 0 := pow_ne_zero k h_phi_ne
 138  have h_pow_succ_ne : phi ^ (k + 1) ≠ 0 := pow_ne_zero (k + 1) h_phi_ne
 139  have h_eq : (1 : ℝ) / phi ^ (k + 1) * phi = 1 / phi ^ k := by
 140    rw [pow_succ]
 141    field_simp
 142  have h1 : (1 + 1 / phi ^ (k + 1) - 1) * phi = (1 / phi ^ (k + 1)) * phi := by
 143    ring
 144  have h2 : (1 + 1 / phi ^ k - 1) = 1 / phi ^ k := by ring
 145  rw [h1, h_eq, h2]
 146
 147/-! ## §4. J-cost separation on the JND ladder -/
 148
 149/-- Every rung-`k` JND has strictly positive J-cost separation from
 150unison (`Cost.Jcost (pitchJND k) > 0`). -/
 151theorem pitchJND_jcost_pos (k : ℕ) : 0 < Cost.Jcost (pitchJND k) := by
 152  apply Cost.Jcost_pos_of_ne_one (pitchJND k) (pitchJND_pos k)
 153  exact ne_of_gt (pitchJND_gt_one k)
 154
 155/-! ## §5. Numerical anchors at canonical rungs -/
 156
 157/-- Rung-`1` JND: `pitchJND 1 = 1 + 1/φ`. -/
 158theorem pitchJND_one : pitchJND 1 = 1 + 1 / phi := by
 159  unfold pitchJND
 160  congr 1
 161  rw [pow_one]
 162
 163/-- Rung-`1` JND lies in the perfect-fifth-class band:
 164`pitchJND 1 ∈ (1.61, 1.62)` (using `1 + 1/φ = φ`). -/
 165theorem pitchJND_one_band :
 166    1.61 < pitchJND 1 ∧ pitchJND 1 < 1.62 := by
 167  rw [pitchJND_one]
 168  -- 1 + 1/φ = φ from φ² = φ + 1
 169  have h_id : 1 + 1 / phi = phi := by
 170    have h_phi_pos : 0 < phi := phi_pos
 171    have h_phi_ne : phi ≠ 0 := phi_ne_zero
 172    have h_phi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
 173    field_simp
 174    nlinarith [h_phi_sq]
 175  rw [h_id]
 176  exact ⟨phi_gt_onePointSixOne, phi_lt_onePointSixTwo⟩
 177
 178/-! ## §6. Master certificate -/
 179
 180/-- **PITCH-PERCEPTION-FROM-PHI-LADDER MASTER CERTIFICATE (Track L6).**
 181
 182Eight clauses, each derived from `Constants.phi` real-arithmetic
 183bounds and `Cost.Jcost` machinery:
 184
 1851. `JND_gt_one`: every JND ratio is strictly greater than unison.
 1862. `JND_pos`: every JND ratio is positive.
 1873. `JND_strictly_decreasing`: rung-`k` JND strictly decreases in `k`.
 1884. `JND_succ_lt`: adjacent rungs strictly improve resolution.
 1895. `JND_increment_geometric`: per-rung improvement is geometric in φ.
 1906. `JND_jcost_pos`: every JND has positive J-cost separation from
 191   unison.
 1927. `JND_one_eq`: rung-1 JND `= 1 + 1/φ`.
 1938. `JND_one_band`: rung-1 JND `∈ (1.61, 1.62)` (closed-form `= φ`).
 194-/
 195structure PitchPerceptionFromPhiLadderCert where
 196  JND_gt_one : ∀ k, 1 < pitchJND k
 197  JND_pos : ∀ k, 0 < pitchJND k
 198  JND_strictly_decreasing : StrictAnti pitchJND
 199  JND_succ_lt : ∀ k, pitchJND (k + 1) < pitchJND k
 200  JND_increment_geometric :
 201    ∀ k, (pitchJND (k + 1) - 1) * phi = pitchJND k - 1
 202  JND_jcost_pos : ∀ k, 0 < Cost.Jcost (pitchJND k)
 203  JND_one_eq : pitchJND 1 = 1 + 1 / phi
 204  JND_one_band : 1.61 < pitchJND 1 ∧ pitchJND 1 < 1.62
 205
 206/-- The master certificate is inhabited. -/
 207def pitchPerceptionFromPhiLadderCert : PitchPerceptionFromPhiLadderCert where
 208  JND_gt_one := pitchJND_gt_one
 209  JND_pos := pitchJND_pos
 210  JND_strictly_decreasing := pitchJND_strict_anti
 211  JND_succ_lt := pitchJND_succ_lt
 212  JND_increment_geometric := pitchJND_increment_geometric
 213  JND_jcost_pos := pitchJND_jcost_pos
 214  JND_one_eq := pitchJND_one
 215  JND_one_band := pitchJND_one_band
 216
 217/-! ## §7. One-statement summary -/
 218
 219/-- **PITCH PERCEPTION FROM THE PHI-LADDER: ONE-STATEMENT THEOREM
 220(Track L6).**
 221
 222Pitch resolution on the auditory φ-ladder forces a discrete
 223just-noticeable-difference (JND) ladder `pitchJND k = 1 + 1/φ^k`
 224for integer rung `k ≥ 0`. Every rung gives a JND strictly greater
 225than unison; rungs are strictly ordered (finer rungs give finer
 226resolution); the per-rung improvement is geometric in φ; every JND
 227has strictly positive J-cost separation from unison; the rung-1 JND
 228equals `1 + 1/φ = φ ∈ (1.61, 1.62)`.
 229-/
 230theorem pitch_perception_one_statement :
 231    -- (1) Every JND > 1.
 232    (∀ k, 1 < pitchJND k) ∧
 233    -- (2) Strictly decreasing.
 234    StrictAnti pitchJND ∧
 235    -- (3) Geometric per-rung improvement.
 236    (∀ k, (pitchJND (k + 1) - 1) * phi = pitchJND k - 1) ∧
 237    -- (4) Positive J-cost separation.
 238    (∀ k, 0 < Cost.Jcost (pitchJND k)) ∧
 239    -- (5) Rung-1 closed form.
 240    pitchJND 1 = 1 + 1 / phi :=
 241  ⟨pitchJND_gt_one,
 242   pitchJND_strict_anti,
 243   pitchJND_increment_geometric,
 244   pitchJND_jcost_pos,
 245   pitchJND_one⟩
 246
 247end
 248
 249end PitchPerceptionFromPhiLadder
 250end MusicTheory
 251end IndisputableMonolith
 252