optimalT60
plain-language theorem explainer
Optimal reverberation time in room acoustics is set to the golden ratio φ in Recognition Science units. Acoustics modelers cite it when mapping J-cost thresholds to empirical Beranek bands for concert halls. The declaration is a direct assignment to the constant phi from the constants module.
Claim. The optimal reverberation time $T_{60}$ equals the golden ratio $φ$.
background
The module expresses the Sabine formula through J-cost on the dimensionless absorption ratio r. Optimal music performance occurs at the golden-section threshold J(φ), which the module identifies with critical damping for concert halls. This produces the structural prediction that optimal T60 equals φ seconds, placing measured halls such as Carnegie (1.89 s) inside the interval (φ, φ²).
proof idea
Direct definition: optimalT60 is assigned exactly the constant phi with no computation or lemmas applied.
why it matters
It supplies the numerical value used by the band theorem proving 1.61 < optimalT60 < 1.62, the over-damped bound optimalT60 > 1, and the RoomAcousticsCert structure. The definition realizes the module claim that optimal concert-hall T60 equals φ, connecting to the self-similar fixed point from the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.