RSACSCert005
plain-language theorem explainer
A certificate bundle for Acoustics domain certificate 5: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Acoustic and ledger-posting arguments cite it as the structural interface that an RS acoustics cost must satisfy. It is a pure structure definition; inhabitants are supplied separately by packing the three sibling lemmas.
Claim. A certificate consists of three properties of the acoustics domain cost $C$ and 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
Module RS_ACS_Cert_005 packages a structural acoustics certificate under the Recognition Science reading that a ledger posting is a recognition event, with a sigma conservation law in the background. Status is structural: zero sorry, zero axiom.
The domain cost is the acoustics-side specialization of the RS J-cost. Upstream, ObserverForcing records that every recognition event has nonnegative cost via Cost.Jcost_nonneg on a positive state. The certificate lifts that nonnegativity (and the diagonal vanishing at equal positive arguments) into an explicit triple of field obligations, together with positivity of a canonical threshold used as a comparison scale.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are the concrete witnesses that later fill the fields.
proof idea
No proof body: this is a structure declaration. It only names the three Prop-valued fields (diagonal vanishing of the domain cost, nonnegativity for positive mass/energy-style arguments, and positivity of the canonical threshold). Inhabitation is deferred to the downstream cert definition, which assigns the three sibling lemmas fieldwise, and to cert_inhabited, which wraps that instance as Nonempty.
why it matters
Gives the typed interface for Acoustics certificate 5 so downstream code can depend on a single inhabited bundle rather than three loose lemmas. Immediate consumers are cert (the canonical inhabitant) and cert_inhabited (Nonempty proof). In the RS acoustics story this is the structural gate that domain cost behaves like a recognition cost: zero on matched postings, never negative, with a positive threshold scale. It sits under the broader forcing picture where J-cost nonnegativity is already forced at the foundation layer; the certificate merely reifies that discipline for the acoustics domain without adding axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.