cert
plain-language theorem explainer
Inhabits the acoustics domain certificate by packaging three structural facts: domain cost vanishes on equal arguments, is nonnegative for positive inputs, and the canonical threshold is positive. Anyone citing the RS acoustics certificate (J(φ)≈0.118 band) uses this witness. Construction is a direct field-wise assembly of three already-proved lemmas.
Claim. There is an acoustics domain certificate whose fields assert: (i) for all $r\neq 0$, the domain cost of $(r,r)$ is zero; (ii) for all $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold (the $J(\varphi)\approx 0.118$ cost level) is strictly positive.
background
The module is Acoustics RS Domain Certificate 3. In Recognition Science the cost functional is the unique $J$ forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$, minimized at the identity $x=1$ with $J(1)=0$. The golden ratio $\varphi$ is the self-similar fixed point (forcing step T6), and $J(\varphi)\approx 0.118$ supplies the canonical cost threshold for this domain.
domainCost is the acoustics-domain specialization of that cost on a pair of positive real arguments (measure vs expectation style). The structure RSACSCert003 packages the three minimal structural obligations any such domain cost must meet: diagonal vanishing, nonnegativity, and a positive threshold. Upstream, nonnegativity of recognition cost is the general fact that $J\ge 0$ on positive reals (ObserverForcing / Cost).
proof idea
Pure structure inhabitant, not a tactic proof. Each of the three fields of RSACSCert003 is filled by the corresponding in-module lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further rewriting or case analysis.
why it matters
Gives a single named witness that the acoustics domain cost satisfies the RS certificate interface: zero on matched arguments, nonnegative, and gated by the $J(\varphi)\approx 0.118$ threshold that the module doc identifies as organizing phi-rung ladder predictions. This is marked a structural theorem (zero sorry, zero axiom). It sits in the acoustics certificate layer rather than in the T0–T8 forcing chain itself, but it inherits $J$-uniqueness (T5) and the forced $\varphi$ (T6) through the cost and threshold definitions. No downstream consumers are recorded yet; the sibling cert_inhabited is the natural next step that treats this witness as evidence the certificate type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.