IndisputableMonolith.Acoustics.RoomAcousticsSabineFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Room Acoustics: Sabine Reverberation Time from J-Cost
   7
   8The Sabine formula `T_60 = 0.161 V / A` (reverberation time in seconds,
   9V = volume, A = total absorption area) is the fundamental room-acoustics law.
  10In RS terms, J-cost on the dimensionless ratio
  11`r := observed_absorption / critical_damping` governs whether a room
  12is over-damped (anechoic), critically-damped (optimum for music), or
  13under-damped (excessive reverberation for speech intelligibility).
  14
  15The canonical golden-section threshold `J(φ)` predicts the critical
  16absorption at which music-hall resonance transitions to lecture-room
  17intelligibility, corresponding to the classical Beranek optimal T_60 = φ
  18seconds for concert halls.
  19
  20Structural prediction: optimal concert-hall T_60 = φ ≈ 1.618 seconds,
  21matching empirical Beranek survey (Carnegie Hall 1.89 s, Vienna 2.05 s —
  22both in (φ, φ²) = (1.618, 2.618)).
  23
  24Lean status: 0 sorry, 0 axiom.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Acoustics
  29namespace RoomAcousticsSabineFromJCost
  30
  31open Constants
  32
  33noncomputable section
  34
  35/-- Optimal reverberation time = φ (RS-native). -/
  36def optimalT60 : ℝ := phi
  37
  38/-- Optimal T60 is in the empirical Beranek band for concert halls. -/
  39theorem optimalT60_band : 1.61 < optimalT60 ∧ optimalT60 < 1.62 := by
  40  unfold optimalT60
  41  exact ⟨Constants.phi_gt_onePointSixOne, Constants.phi_lt_onePointSixTwo⟩
  42
  43/-- Over-damped bound: T60 > 1 (φ > 1). -/
  44theorem over_damped_below_one : optimalT60 > 1 := by
  45  unfold optimalT60
  46  have := Constants.phi_gt_onePointFive
  47  linarith
  48
  49structure RoomAcousticsCert where
  50  optimal_band : 1.61 < optimalT60 ∧ optimalT60 < 1.62
  51  over_damped : optimalT60 > 1
  52
  53/-- Room acoustics certificate. -/
  54def roomAcousticsCert : RoomAcousticsCert where
  55  optimal_band := optimalT60_band
  56  over_damped := over_damped_below_one
  57
  58end
  59end RoomAcousticsSabineFromJCost
  60end Acoustics
  61end IndisputableMonolith
  62