cert
plain-language theorem explainer
Packages three structural properties of the acoustics domain cost into a single certificate record: diagonal vanishing, nonnegativity, and a positive canonical threshold. Anyone citing Acoustics RS Domain Certificate 10 uses this inhabitant. The body is a pure structure assembly of three already-proved field 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
Recognition Science domain certificates package the minimal algebraic properties a cost functional must satisfy before it can serve as a falsifiable RS interface. In this acoustics module the cost is the domain cost on pairs of positive reals (imported from the Cost layer and Constants), and the threshold is a fixed positive scale against which acoustic observables are compared.
The certificate structure demands three facts: the cost vanishes on the diagonal away from zero (identity events cost nothing), the cost is nonnegative on the positive orthant, and the canonical threshold is positive. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via the J-cost minimum at $x=1$.
The module frames itself as a structural theorem with zero sorry and zero axioms, and states the RS falsifier convention: any 5-sigma contradiction against the certificate closes the framework.
proof idea
Pure structure inhabitant. The three fields are filled by the in-module lemmas that already prove diagonal vanishing of the domain cost, nonnegativity of the domain cost on positive arguments, and positivity of the canonical threshold. No extra algebra is performed at this site.
why it matters
This is the concrete witness that Acoustics RS Domain Certificate 10 is inhabited. Downstream consumers (none linked yet in the graph) can assume the three cost axioms without re-proving them. It sits in the broader RS pattern of domain certificates that turn J-cost nonnegativity and identity-minimum structure into auditable, falsifiable interfaces. The module's own falsifier clause (any 5-sigma contradiction closes the framework) makes the certificate the gate that acoustic predictions must pass. It does not itself touch the forcing chain T0-T8, but inherits cost nonnegativity from the same J-cost layer that T5 uniqueness governs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.