rt60_ratio
plain-language theorem explainer
The reverberation time RT60 between adjacent regimes on the phi-ladder satisfies rt60(k+1)/rt60(k) = phi for every natural number k. Acousticians working inside Recognition Science cite this to lock in the scaling law across the five canonical regimes. The proof is a direct algebraic reduction: unfold the power definition of rt60, invoke positivity of phi^k, rewrite the division, apply the successor exponent rule, and finish with ring.
Claim. For every natural number $k$, the ratio of reverberation times satisfies $$rt60(k+1)/rt60(k) = phi$$ where $rt60(k) := phi^k$.
background
The module derives room acoustics from the phi-ladder under configDim D=5, yielding five regimes (anechoic to echoic). Reverberation time is introduced via the upstream definition rt60(k) := phi^k, which encodes exponential growth forced by the self-similar fixed point phi. The module documentation states that adjacent-regime ratio equals phi, and the present theorem supplies the formal statement of that scaling.
proof idea
Unfold rt60 to replace both sides by powers of phi. Establish positivity of phi^k via pow_pos. Rewrite the division equation using div_eq_iff on the nonzero denominator. Apply pow_succ to the numerator. Close the resulting polynomial identity with ring.
why it matters
The result populates the phi_ratio field of roomAcousticsCert, the certificate that bundles regime count, the ratio, and positivity. It directly realizes the module claim that RT60 scales on the phi-ladder with adjacent ratio phi. In the larger framework this confirms the phi-ladder structure (T6) applied to acoustics, consistent with the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.