Pith. sign in
module module moderate

IndisputableMonolith.Acoustics.RoomAcousticsFromPhiLadder

show as:
view Lean formalization →

The module derives room acoustics quantities from the phi ladder in Recognition Science. It defines regimes, counts, rt60 metrics and certificates using the time quantum from Constants. Acoustics and RS researchers would cite it to connect fundamental scales to reverberation parameters. The module consists entirely of definitions and supporting certificates.

claimDefines $\text{RoomAcousticRegime}$, $\text{rt60}$, $\text{rt60_ratio}$, $\text{rt60_pos}$ and $\text{RoomAcousticsCert}$ from the phi ladder with base time quantum $\tau_0 = 1$ tick.

background

The module sits inside the Recognition Science framework that derives physics from a single functional equation. It imports the Constants module whose sole documented content is the fundamental RS time quantum $\tau_0 = 1$ tick.

Sibling definitions introduce RoomAcousticRegime as a classification, roomAcousticRegime_count, the reverberation-time functions rt60, rt60_ratio and rt60_pos, plus the certificate RoomAcousticsCert. All are constructed on the phi ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the acoustics domain inside Recognition Science and is positioned to feed parent derivations that apply the phi ladder and eight-tick octave (T7) to concrete physical regimes. No downstream uses are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)