RoomAcousticsCert
plain-language theorem explainer
RoomAcousticsCert packages the two inequalities 1.61 < optimalT60 < 1.62 and optimalT60 > 1 into a single structure. Acoustics researchers deriving reverberation times from the J-cost on absorption ratios cite the certificate to confirm agreement with Beranek's empirical optimum near 1.618 s. The definition is assembled by direct reference to the optimalT60 definition together with the band and damping lemmas.
Claim. The structure asserts that the optimal reverberation time $T_{60}^*$ satisfies $1.61 < T_{60}^* < 1.62$ and $T_{60}^* > 1$, where $T_{60}^*$ is obtained from the J-cost functional on the absorption ratio.
background
The module derives room acoustics from the J-cost on the dimensionless ratio of observed absorption to critical damping. The classical Sabine formula gives reverberation time as $T_{60} = 0.161 V / A$; the RS-native optimum occurs at the golden-section threshold $J(φ)$ and is defined by setting optimalT60 to phi. Upstream, the phi-ladder RoomAcousticsCert structure requires exactly five regimes, successive rt60 ratios equal to phi, and strictly positive rt60 values.
proof idea
Structure definition that supplies the optimal band field from the optimalT60_band lemma and the over_damped field from the over_damped_below_one lemma, both resting on the constant definition optimalT60 := phi.
why it matters
This definition supplies the numerical bounds required to instantiate the general RoomAcousticsCert structure in the phi-ladder acoustics module. It closes the link between the abstract phi-ladder properties and the empirical T60 band for concert halls, consistent with the J-uniqueness theorem and the self-similar fixed point phi. The downstream roomAcousticsCert definition in this module uses it to produce the full certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.