over_damped_below_one
plain-language theorem explainer
The theorem establishes that the optimal reverberation time exceeds one second in Recognition Science units. Acousticians applying the Sabine formula to classify damping regimes would cite this bound when distinguishing over-damped rooms. The proof reduces the claim directly to the known lower bound on the golden ratio via unfolding and linear arithmetic.
Claim. The optimal reverberation time satisfies $T_{60} > 1$.
background
The module derives room acoustics from the J-cost function on the dimensionless ratio of observed absorption to critical damping. This ratio determines whether a room is over-damped, critically damped at the golden-section threshold, or under-damped. The definition optimalT60 sets the optimal reverberation time to phi, matching the empirical Beranek band for concert halls as noted in the module documentation.
proof idea
The proof is a one-line wrapper that unfolds optimalT60 to phi, invokes the lemma phi_gt_onePointFive establishing phi > 1.5, and applies linarith to conclude phi > 1.
why it matters
This theorem supplies the over_damped field in the roomAcousticsCert definition. It closes the bound for the over-damped regime in the derivation of Sabine reverberation time from J-cost. The result supports the structural prediction that optimal concert-hall T60 equals phi seconds and aligns with the phi fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.