cert
plain-language theorem explainer
Packages three acoustic-domain facts (vanishing self-cost, nonnegativity of domain cost, positive canonical threshold) into one RSACSCert004 record. Cited by anyone needing a single certificate object for the D=3 Count Law / gap-45 acoustics module. Construction is pure field assignment of already-proved sibling lemmas.
Claim. There is 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_004 is the acoustics domain certificate tied to the Count Law $2^D-1=7$ at $D=3$ and the forced gap identity $\mathrm{gap}\text{-}45=D^2(D+2)=45$. Status is structural: zero sorry, zero axiom.
The certificate structure RSACSCert004 packages three Prop fields about a real-valued domain cost and a canonical threshold: diagonal vanishing off zero, nonnegativity on the positive quadrant, and positivity of the threshold. Domain cost is the acoustics-side cost functional (imported Cost/Constants stack); nonnegativity is the local specialization of the global recognition-cost fact that every recognition event has nonnegative J-cost.
Upstream, ObserverForcing records that cost is nonnegative via Jcost_nonneg on positive state. The siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields before this definition bundles them.
proof idea
Structure construction, not a tactic proof. The three fields of RSACSCert004 are filled by direct assignment:
cost_at_eqfrom the sibling lemma that domain cost vanishes on the diagonal for nonzero $r$;cost_nonnegfrom the sibling nonnegativity lemma on positive arguments (itself the acoustics specialization of foundationcost_nonneg/Jcost_nonneg);threshold_posfrom the sibling positivity of the canonical threshold. No further rewriting or case analysis.
why it matters
Gives a single named inhabitant of the acoustics certificate structure so downstream acoustics or forcing code can depend on one object rather than three separate lemmas. The module doc frames the certificate as the structural witness for Count Law $2^D-1=7$ at $D=3$ and gap-45 $=D^2(D+2)$, aligning with forcing-chain landmark T8 (three spatial dimensions) and the eight-tick octave counting $2^3$.
No used_by edges are recorded yet; the immediate consumer in-module is the inhabitedness wrapper. The declaration closes the certificate interface for this acoustics slice without adding new physics content beyond the three field lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.