cert
plain-language theorem explainer
Packages the three acoustic J-cost side conditions (vanishing on the diagonal, non-negativity, positive threshold) into a single certificate for room-impulse modeling. Anyone deriving RT60 absorption from the Recognition cost would cite this bundle. The definition is a pure structure instance that wires three already-proved component lemmas.
Claim. There is a certificate asserting: the acoustic domain cost $C$ satisfies $C(r,r)=0$ for every $r\neq 0$; $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical absorption threshold is strictly positive.
background
This module treats room impulse response through the Recognition J-cost. The classical reverberation time is $T_{60}=0.161,V/(A\alpha)$, and the plan identifies the canonical absorption coefficient near the diffuse-field optimum with $\alpha\approx J(\varphi)$, where $J$ is the unique cost forced by the Recognition Composition Law ($J(x)=(x+x^{-1})/2-1$).
The local domain cost $C(m,e)$ is the acoustic specialization of that J-cost on positive mode and excitation scales. Equilibrium means matched arguments: $C(r,r)=0$ for $r\neq 0$. Non-negativity is the acoustic reading of the general fact that every recognition event has non-negative cost (upstream cost_nonneg via $J\ge 0$).
RoomImpulseCert is the structure that packages exactly those three obligations: diagonal vanishing, non-negativity for positive arguments, and positivity of the canonical threshold used as the absorption cutoff.
proof idea
Not a tactic proof: a structure-value definition. The three fields of RoomImpulseCert are filled by the sibling lemmas domainCost_at_equilibrium (diagonal vanishing), domainCost_nonneg (non-negativity on positive reals), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the room-impulse certificate so downstream acoustics developments can assume the J-cost side conditions without re-proving them. The module frames this as a structural theorem (zero sorry, zero axiom) linking RT60 absorption to $J(\varphi)$ on the phi-ladder forced at T5–T6.
No further used_by edges are recorded yet; the immediate consumer is the sibling inhabitance fact and any later RT60 or diffuse-field derivation that needs a bundled certificate rather than three loose lemmas. It closes the local packaging step of the Plan v7 acoustics pass without touching open forcing or mass-ladder obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.