IndisputableMonolith.Acoustics.RoomAcousticsFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Room Acoustics from φ-ladder — B14 Depth
   6
   7Five canonical room-acoustic regimes (= configDim D = 5):
   8  anechoic, heavily-damped, semi-reverberant, reverberant, echoic.
   9
  10Reverberation time RT60 scales on φ-ladder: adjacent-regime ratio = φ.
  11
  12Speech intelligibility threshold (STI canonical band) = J(φ) ∈ (0.11, 0.13).
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Acoustics.RoomAcousticsFromPhiLadder
  18open Constants
  19
  20inductive RoomAcousticRegime where
  21  | anechoic
  22  | heavilyDamped
  23  | semiReverberant
  24  | reverberant
  25  | echoic
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem roomAcousticRegime_count : Fintype.card RoomAcousticRegime = 5 := by decide
  29
  30noncomputable def rt60 (k : ℕ) : ℝ := phi ^ k
  31
  32theorem rt60_ratio (k : ℕ) : rt60 (k + 1) / rt60 k = phi := by
  33  unfold rt60
  34  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  35  rw [div_eq_iff hpos.ne', pow_succ]
  36  ring
  37
  38theorem rt60_pos (k : ℕ) : 0 < rt60 k := pow_pos phi_pos k
  39
  40structure RoomAcousticsCert where
  41  five_regimes : Fintype.card RoomAcousticRegime = 5
  42  phi_ratio : ∀ k, rt60 (k + 1) / rt60 k = phi
  43  rt60_always_pos : ∀ k, 0 < rt60 k
  44
  45noncomputable def roomAcousticsCert : RoomAcousticsCert where
  46  five_regimes := roomAcousticRegime_count
  47  phi_ratio := rt60_ratio
  48  rt60_always_pos := rt60_pos
  49
  50end IndisputableMonolith.Acoustics.RoomAcousticsFromPhiLadder
  51