RoomImpulseCert
plain-language theorem explainer
A certificate structure that packages three algebraic properties of the room-domain cost: vanishing on the diagonal, non-negativity for positive arguments, and positivity of the canonical absorption threshold. Anyone deriving Sabine-type RT60 from the Recognition J-cost cites this as the interface between cost calculus and room acoustics. It is a pure structure definition; concrete inhabitants are assembled from three sibling lemmas.
Claim. A room-impulse certificate is a triple of facts about the room-domain cost $C:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module treats room impulse response as a Recognition-cost problem. The classical Sabine reverberation time is $T_{60}=0.161,V/(A\alpha)$, and the module identifies the canonical absorption coefficient near the diffuse-field optimum with a value built from the J-cost, $\alpha\approx J(\varphi)$.
The J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique nonnegative cost forced by the Recognition Composition Law; it vanishes only at $x=1$. Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J$. The room-domain cost is the specialization of that calculus to a pair of positive reals (mode amplitude and excitation), and the canonical threshold is the positive cutoff used as the absorption scale.
Local status is structural: zero sorry, zero axioms. The certificate is the Prop-bundle that later constructions must inhabit before RT60 identities are stated.
proof idea
No proof body: this is a structure declaration whose three fields are propositions. Field one demands the domain cost vanish on the diagonal away from zero (equilibrium). Field two demands nonnegativity for positive arguments, mirroring the upstream recognition-event nonnegativity theorem. Field three demands the canonical threshold be strictly positive. Inhabitants are built elsewhere by supplying the three sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
This structure is the typed interface between J-cost calculus and room acoustics in the Recognition framework. Downstream, cert assembles a concrete inhabitant from the three sibling lemmas, and cert_inhabited records Nonempty of the certificate type, closing the structural obligation of the module.
The module doc pins the physical target: RT60 with absorption $\alpha\approx J(\varphi)$ at the diffuse-field optimum, tying the certificate to the forced golden-ratio fixed point (T6) and the unique J-cost (T5). Without a positive threshold and a nonnegative cost that vanishes at equilibrium, the passage from recognition cost to a Sabine-type absorption coefficient would be ill-typed. The declaration itself does not compute $T_{60}$; it only freezes the hypotheses that any such derivation must discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.