cert
plain-language theorem explainer
Packages three structural facts about the acoustics domain cost into a single certificate record: the cost vanishes on the diagonal, stays nonnegative for positive model and experiment values, and the canonical threshold is positive. Anyone needing a certified acoustics domain instance cites this inhabitant. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There exists an acoustics domain certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_ACS_Cert_007 is Acoustics Domain Certificate 7 in the Recognition Science stack. The stated pattern is $\phi^k$ scaling of an observable quantity $k$, required exact within 1%, and the module is marked a structural theorem (zero sorry, zero axiom).
The certificate structure demands three properties of the local domain cost: it vanishes when model equals experiment (off zero), it is nonnegative on the positive quadrant, and a fixed positive threshold is available for comparison. Domain cost is the acoustics-side specialization of the recognition cost; upstream, the foundation lemma cost_nonneg records that every recognition event has nonnegative J-cost, via nonnegativity of $J$ on positive reals.
Sibling lemmas already establish the three field obligations for this domain: diagonal vanishing, nonnegativity of domain cost, and positivity of the canonical threshold.
proof idea
Pure structure construction. The three fields of the certificate are filled by direct assignment of the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or algebraic reduction occurs at this site; it is an inhabitant assembly step.
why it matters
Gives a single named inhabitant of the Acoustics Certificate 7 structure so downstream acoustics arguments can assume the three cost axioms as a bundle rather than re-importing each lemma. The module frames this as the structural half of the $\phi^k$ scaling pattern for acoustics observables (exact within 1%). It sits on the same cost nonnegativity spine as the foundation observer-forcing result that every recognition event has nonnegative J-cost. No external used-by edges are recorded yet; the immediate consumer in-module is the inhabitedness witness for the same certificate type. Framework landmarks touched only indirectly: J-cost nonnegativity (T5 lineage) and $\phi$-scaling of observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.