cert
plain-language theorem explainer
Packages three elementary properties of the RT60 domain cost into a single certificate record: diagonal vanishing, non-negativity on positive arguments, and positivity of the canonical threshold. Anyone citing the RS room-acoustics RT60 layer uses this bundle rather than the three lemmas separately. The definition is a pure structure instance that wires the sibling proofs into the certificate fields.
Claim. There is a certificate recording that the RT60 domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical RT60 threshold $T$ obeys $T>0$.
background
The module treats reverberation time RT60 in Recognition Science units. Empirically, studio rooms sit near $0.2$–$0.5,\mathrm{s}$; the RS ladder writes $\mathrm{RT60}=\varphi^k\cdot 0.1,\mathrm{s}$, so $\varphi^3\cdot 0.1\approx 0.424,\mathrm{s}$ lands in the studio band and $\varphi^5\cdot 0.1\approx 1.1,\mathrm{s}$ matches concert halls.
Domain cost here is the local mismatch functional on measured versus expected RT60 scales (built from the global $J$-cost). The certificate structure demands three facts: cost vanishes when measurement equals expectation on the nonzero diagonal, cost is nonnegative for positive inputs, and the canonical threshold used to gate acceptable rooms is strictly positive. Nonnegativity of recognition cost is the upstream forcing fact that any recognition event has $J$-cost $\ge 0$.
proof idea
One-line structure instance. Each field of RT60Cert is filled by the matching in-module lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra algebra is performed at this site.
why it matters
Gives the acoustics layer a single inhabited certificate object rather than three loose lemmas, matching the module's STRUCTURAL THEOREM status (zero sorry, zero axiom). It sits on the same cost-nonnegativity spine used throughout RS forcing (ObserverForcing), specialized to RT60 scales on the $\varphi$-ladder. No downstream consumers are wired yet in the graph; the natural next step is an inhabitedness or acceptance theorem that quotes this certificate when comparing a room's measured RT60 against the canonical threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.