cert
plain-language theorem explainer
Packages three elementary properties of the acoustics domain cost into a single certificate record: vanishing on the diagonal, non-negativity off the identity, and a strictly positive canonical threshold. Anyone citing the RS acoustics structural certificate (forcing chain T5–T8) uses this inhabitant. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There exists an acoustics domain certificate whose three fields assert: (i) the domain cost of any nonzero ratio against itself is zero, $\mathrm{domainCost}(r,r)=0$ for $r\neq 0$; (ii) for positive mass and energy parameters the domain cost is non-negative; (iii) the canonical threshold is strictly positive.
background
This module is the second RS acoustics domain certificate. Per the module header it is a structural theorem with zero sorry and zero axioms, aligned to the forcing chain T5–T8 (J-uniqueness through D = 3).
The certificate structure RSACSCert002 packages three Prop fields about a real-valued domain cost on mass/energy pairs and a fixed positive threshold. Domain cost is the acoustics-side specialization of the RS recognition cost; upstream, the foundation lemma cost_nonneg states that every recognition event has non-negative cost via non-negativity of the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$.
Sibling lemmas already establish the three fields: diagonal vanishing of domain cost, its non-negativity for positive arguments, and positivity of the canonical threshold. The present declaration simply inhabits the structure with those proofs.
proof idea
One-line structure inhabitant. The three fields of RSACSCert002 are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional tactic work; the definition is pure record assembly. The non-negativity field ultimately rests on the foundation fact that J-cost (hence recognition cost) is non-negative.
why it matters
Gives a single named witness that the acoustics domain cost satisfies the three structural axioms expected of an RS cost functional: zero on self-comparison, non-negativity, and a positive decision threshold. The module frames this as part of the T5–T8 forcing chain (J-uniqueness, $\varphi$ fixed point, eight-tick octave, $D=3$), so downstream acoustics arguments can cite one certificate rather than three separate lemmas.
No downstream users are recorded yet (used_by is empty), so the immediate role is archival: a clean, axiom-free package for the acoustics side of the RS cost interface. It does not itself derive new physics constants; it certifies that the local cost object is well-formed for later comparison against the global J-cost and the $\varphi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.