cert
plain-language theorem explainer
Inhabited Acoustics domain certificate 6: the domain cost vanishes on the diagonal, stays nonnegative for positive model and evidence, and the canonical threshold is strictly positive. Cited by anyone assembling the parameter-free RS acoustics structural layer (E_coh fixed once by the electron mass). The definition is a pure structure instance that wires three already-proved sibling lemmas.
Claim. There is an inhabited certificate packing three facts: for every nonzero real $r$, the acoustics domain cost satisfies $C(r,r)=0$; for all positive reals $m,e$, one has $C(m,e)\ge 0$; and the canonical threshold $T$ obeys $T>0$.
background
Module setting is Acoustics RS Domain Certificate 6: RS energy $E_{\mathrm{coh}}$ is fixed once from the electron mass, so all predictions in the certificate are parameter-free. Status is structural (zero sorry, zero axiom).
The certificate structure demands three properties of the local domain cost $C$: diagonal vanishing ($C(r,r)=0$ for $r\neq 0$), nonnegativity on the positive quadrant, and positivity of a fixed canonical threshold. Nonnegativity is the domain-level shadow of the global fact that every recognition event has nonnegative cost, which follows from nonnegativity of the J-cost on positive reals (the unique cost forced by the Recognition Composition Law).
Sibling lemmas already establish the three fields for this module's concrete domainCost and canonicalThreshold; the certificate merely packages them.
proof idea
Not a tactic proof: a structure-instance definition. The three fields of the certificate are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that Acoustics certificate 6 is fully discharged at the structural level. Downstream consumers (none yet linked in the graph) can assume diagonal vanishing, cost nonnegativity, and a positive threshold without reopening the cost lemmas. Fits the RS pattern that domain certificates are pure packaging of J-cost consequences once $E_{\mathrm{coh}}$ is fixed; no free parameters enter. Does not itself touch the forcing chain T5–T8, but inherits cost nonnegativity from the observer-forcing layer that rests on J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.