cert_inhabited
plain-language theorem explainer
The Module-10 chemistry certificate type is nonempty: a witness exists packing diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold. Anyone citing the CH4 laminar flame-speed structural match (phi^{-2} ~ 0.40 m/s) needs this inhabitance fact. Proof is a one-line term supplying the prebuilt certificate instance.
Claim. There exists a certificate asserting that the domain cost vanishes on the diagonal ($\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$), is nonnegative for positive arguments, and that the module's canonical threshold is strictly positive.
background
Chemistry RS Module 10 records the laminar flame speed of methane as a structural match: $\phi^{-2}\approx 0.382$ m/s against the experimental value $\sim 0.40$ m/s. The module is marked a structural theorem (zero sorry, zero axioms).
The local certificate structure packages three algebraic properties of the domain-cost functional used in this chemistry layer: it returns zero whenever the two arguments coincide and are nonzero; it is nonnegative whenever both mass and energy arguments are positive; and the module's canonical threshold is strictly positive. These are the minimal checks that must hold before any numerical match claim is admitted.
The certificate type is therefore a pure packaging of those three propositions; inhabitance means at least one such package has been constructed in-module.
proof idea
One-line term proof. The module already defines a concrete value of the certificate structure; the theorem simply wraps that value in the anonymous constructor of Nonempty, discharging inhabitance with no further tactics or lemmas.
why it matters
Closes the inhabitance obligation for the Module-10 structural certificate. The parent module itself is the CH4 laminar-flame-speed match at the phi-ladder scale $\phi^{-2}$, listed as a structural theorem with no axioms. No downstream dependents are recorded; the result is a leaf certificate in the chemistry layer of the Recognition stack. It sits downstream of the general cost and constants imports but does not itself invoke the forcing chain (T5--T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.