cert
plain-language theorem explainer
Packages three structural facts about the acoustics domain cost into a single certificate: diagonal vanishing, non-negativity for positive arguments, and a strictly positive canonical threshold. Cited by anyone invoking the zero-parameter RS acoustics certificate (exact J(φ)=φ−3/2). Proof is a structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that the acoustics 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 threshold $T$ obeys $T>0$.
background
This module is Acoustics RS Domain Certificate 8: a zero-parameter structural package. The cost is the RS J-cost specialized to an acoustics model-vs-experiment comparison; the module states the exact identity $J(\varphi)=\varphi-3/2\approx 0.118$ with no fitted constants.
The structure being inhabited asks for three properties only: the domain cost vanishes on the diagonal (model equals experiment), stays non-negative for positive model and experiment values, and the canonical threshold used as a decision cutoff is strictly positive. Upstream, non-negativity of recognition cost is the general fact that every recognition event has $J$-cost $\ge 0$ (ObserverForcing), specialized here to the acoustics domain cost.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos already discharge those three obligations; this declaration only assembles them.
proof idea
Pure structure construction. The three fields of RSACSCert008 are filled by direct assignment to the sibling proofs domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra algebra or tactics; the work lives in those three lemmas.
why it matters
Gives a single named witness that the acoustics domain meets the RS certificate interface: diagonal cost zero, cost non-negative, threshold positive. That is the structural half of the module claim "RS zero-param: $J(\varphi)=\varphi-3/2$ exact, no fitted constants," status structural theorem (0 sorry, 0 axiom).
In the broader framework it sits under the J-uniqueness forcing (T5) and the non-negativity of recognition cost: the acoustics cost is an instance of the same $J$, so the certificate is a domain-level packaging of foundation facts rather than a new dynamical law. No downstream consumers are recorded yet; the immediate role is to close the certificate record and support cert_inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.