rt60_pos
plain-language theorem explainer
Reverberation time RT60(k) equals phi to the power k and remains strictly positive for every natural number k. Acoustics modelers cite the result when certifying the five-regime classification on the phi-ladder. The proof is a one-line wrapper applying the lemma that positive bases remain positive under natural-number exponentiation.
Claim. For every natural number $k$, the reverberation time $RT_{60}(k) := phi^k$ satisfies $RT_{60}(k) > 0$.
background
The module introduces five canonical room-acoustic regimes (anechoic, heavily-damped, semi-reverberant, reverberant, echoic) with configDim D = 5. Reverberation time RT60 scales on the phi-ladder with adjacent-regime ratio equal to phi; speech intelligibility threshold equals J(phi) in (0.11, 0.13). The upstream definition sets rt60(k) := phi ^ k. The theorem relies on this definition together with the positivity of phi.
proof idea
The proof is a one-line wrapper that applies pow_pos to phi_pos at exponent k.
why it matters
The result supplies the rt60_always_pos field inside the roomAcousticsCert definition. It anchors the acoustics model to the Recognition Science phi-ladder, consistent with T6 forcing phi as the self-similar fixed point and the forcing chain through T7 eight-tick octave. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.