IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Speech Intelligibility from J-Cost on Signal-to-Noise Ratio
   7
   8Speech intelligibility (measured by SII, STI, or word-recognition score)
   9is governed by recognition cost on the signal-to-noise ratio
  10`r := signal_power / noise_power` measured in the relevant frequency
  11bands. The intelligibility-1 condition is `r = 1` (signal matches noise
  12threshold) at zero J-cost. Below `r = 1`, J-cost rises and intelligibility
  13drops.
  14
  15The clinical analog: the speech-reception threshold (SRT) is defined as
  16the SNR at which 50 % of words are recognised; healthy adults perform at
  17SRT ≈ -7 dB, with `r ≈ 0.2`. Hearing-impaired listeners show SRT shifts
  18of +5 to +15 dB (one to three φ-rungs of recognition-cost penalty).
  19
  20Lean status: 0 sorry, 0 axiom.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Acoustics
  25namespace SpeechIntelligibilityFromJCost
  26
  27open Constants Cost
  28
  29noncomputable section
  30
  31/-- Speech-recognition J-cost on the SNR ratio. -/
  32def srCost (r : ℝ) : ℝ := Cost.Jcost r
  33
  34theorem srCost_zero_at_threshold : srCost 1 = 0 := Cost.Jcost_unit0
  35
  36theorem srCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  37    srCost r = srCost r⁻¹ := Cost.Jcost_symm hr
  38
  39theorem srCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ srCost r :=
  40  Cost.Jcost_nonneg hr
  41
  42theorem srCost_pos_off_threshold {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  43    0 < srCost r := Cost.Jcost_pos_of_ne_one r hr hne
  44
  45/-- Hearing-loss penalty at φ-step `k` of SNR degradation. -/
  46def hearingLossPenalty (k : ℕ) : ℝ := srCost (phi ^ (-(k : ℤ)))
  47
  48/-- The hearing-loss penalty at zero rungs is zero. -/
  49theorem hearingLossPenalty_zero : hearingLossPenalty 0 = 0 := by
  50  unfold hearingLossPenalty
  51  simp
  52  exact Cost.Jcost_unit0
  53
  54/-- The penalty is nonnegative at every rung. -/
  55theorem hearingLossPenalty_nonneg (k : ℕ) : 0 ≤ hearingLossPenalty k := by
  56  unfold hearingLossPenalty
  57  apply Cost.Jcost_nonneg
  58  exact zpow_pos Constants.phi_pos _
  59
  60structure SpeechIntelligibilityCert where
  61  threshold_zero : srCost 1 = 0
  62  reciprocal_symm : ∀ {r : ℝ}, 0 < r → srCost r = srCost r⁻¹
  63  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ srCost r
  64  penalty_zero : hearingLossPenalty 0 = 0
  65  penalty_nonneg : ∀ k : ℕ, 0 ≤ hearingLossPenalty k
  66
  67/-- Speech-intelligibility-from-J-cost certificate. -/
  68def speechIntelligibilityCert : SpeechIntelligibilityCert where
  69  threshold_zero := srCost_zero_at_threshold
  70  reciprocal_symm := srCost_reciprocal_symm
  71  cost_nonneg := srCost_nonneg
  72  penalty_zero := hearingLossPenalty_zero
  73  penalty_nonneg := hearingLossPenalty_nonneg
  74
  75end
  76end SpeechIntelligibilityFromJCost
  77end Acoustics
  78end IndisputableMonolith
  79