roomAcousticsCert
plain-language theorem explainer
roomAcousticsCert constructs the acoustics certificate by wiring the optimal T60 band theorem and the over-damped bound into the RoomAcousticsCert structure. Acoustics researchers applying Recognition Science would cite it when verifying that J-cost yields the Beranek-optimal reverberation interval near 1.618 s. The proof is a direct field assignment in the structure definition.
Claim. A RoomAcousticsCert is constructed by setting its optimal_band field to the proposition $1.61 < T_{60} < 1.62$ and its over_damped field to $T_{60} > 1$, where $T_{60}$ is the reverberation time at the J-cost critical-damping threshold.
background
The module reinterprets the classical Sabine formula $T_{60} = 0.161 V / A$ through the J-cost on the dimensionless absorption ratio $r$. Critical damping occurs at the golden-section value $J(φ)$, predicting optimal concert-hall reverberation of $φ$ seconds. This matches Beranek's empirical band (1.61, 1.62) s for halls such as Carnegie and Vienna, both lying in $(φ, φ^2)$.$ The RoomAcousticsCert structure collects the band membership and the over-damped inequality $T_{60} > 1$. It extends the phi-ladder certificate from RoomAcousticsFromPhiLadder, which requires five regimes, phi-ratio scaling of successive rt60 values, and positivity.
proof idea
The definition is a one-line structure constructor. It populates the optimal_band field with the result of optimalT60_band and the over_damped field with over_damped_below_one. Both source theorems reduce to inequalities on the constant phi via Constants.phi_gt_onePointSixOne and Constants.phi_gt_onePointFive.
why it matters
This supplies the Sabine-derived certificate that the downstream RoomAcousticsFromPhiLadder.roomAcousticsCert consumes to prove the five-regime count and phi-ratio property. It closes the link from J-cost to the acoustic observables predicted by the T5 J-uniqueness and T6 phi fixed point. The module notes that this yields the structural prediction optimal T60 = φ, consistent with survey data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.