cert
plain-language theorem explainer
Packages three acoustic-domain cost facts into one RSACSCert005 witness: diagonal vanishing, nonnegativity, and a positive canonical threshold. Anyone citing the acoustics domain certificate (ledger posting as recognition event, sigma conservation) uses this bundle. The body is a pure structure constructor that wires three sibling lemmas; no new mathematics is proved here.
Claim. There is a certificate record asserting: (i) for every nonzero real $r$, the acoustic domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module RS_ACS_Cert_005 is the fifth acoustics domain certificate in the Recognition Science mirror. The local setting equates ledger posting with a recognition event and records a sigma conservation law; the module is marked structural (zero sorry, zero axiom).
The certificate structure demands three properties of the acoustic domain cost $C$ and of a fixed positive threshold. Domain cost is the acoustics specialization of the RS J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states.
Sibling lemmas in this file establish the three fields: diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold.
proof idea
One-line structure inhabitation. The definition supplies cost_at_eq from domainCost_at_eq, cost_nonneg from domainCost_nonneg, and threshold_pos from canonicalThreshold_pos. No tactics, no rewriting, no new lemmas: pure field packing into RSACSCert005.
why it matters
Gives a single named witness that the acoustics domain meets the RS certificate interface (cost vanishes on matched posts, never goes negative, threshold is strictly positive). That interface is how the framework treats ledger posting as a recognition event under sigma conservation.
No downstream consumers are recorded yet in the graph, so this is presently a leaf certificate rather than a lemma feeding a larger theorem. It sits in the acoustics track of the structural certificates and inherits the global J-cost nonnegativity story (T5 uniqueness of $J$, cost minimum at the identity). It does not itself touch the forcing chain steps T6–T8, the mass ladder, or the alpha band; those remain outside scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.