optimalT60_band
plain-language theorem explainer
Optimal reverberation time T60 equals phi and satisfies 1.61 < T60 < 1.62. Acoustics researchers cite this when linking J-cost on absorption ratios to the Sabine formula for concert-hall resonance. The proof is a one-line wrapper that unfolds optimalT60 to phi and applies the two pre-proved bounds on phi.
Claim. $1.61 < T_{60} < 1.62$ where $T_{60} := phi$ is the optimal reverberation time in seconds.
background
The module derives Sabine reverberation T60 = 0.161 V / A from J-cost on the ratio r = observed absorption over critical damping. OptimalT60 is defined as phi, the self-similar fixed point that marks the transition from over-damped to critically damped rooms. Upstream lemmas establish the numerical bounds: phi_gt_onePointSixOne shows phi > 1.61 via sqrt(5) comparison, while phi_lt_onePointSixTwo shows phi < 1.62. The Constants structure supplies these RS-native values.
proof idea
Unfold optimalT60 to expose phi, then apply the conjunction of Constants.phi_gt_onePointSixOne and Constants.phi_lt_onePointSixTwo.
why it matters
The theorem supplies the optimal_band field inside roomAcousticsCert, which certifies the full acoustics model. It realizes the module prediction that optimal concert-hall T60 equals phi and matches the empirical Beranek interval, consistent with the T6 phi fixed point in the forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.