cert
plain-language theorem explainer
Certificate packing three structural properties of the methane laminar flame-speed cost: diagonal vanishing, non-negativity, and a positive canonical threshold. Anyone auditing Chemistry Module 10's MATCH claim (φ^{-2} ≈ 0.40 m/s) cites this witness. Proof is a pure structure assembly wiring three local lemmas into the certificate fields.
Claim. There is a certificate asserting: the domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$); $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold is strictly positive.
background
Chemistry RS Module 10 treats the laminar flame speed of methane. The module claims a MATCH: $\phi^{-2}\approx 0.382$ m/s against the experimental $\sim 0.40$ m/s, and is marked as a structural theorem (zero sorry, zero axioms).
The domain cost is the local discrepancy functional between a model value and an experimental value, in the style of the global J-cost. The certificate structure packages the three elementary interface properties needed before that MATCH can be read as a recognition-cost statement: cost vanishes when model equals experiment, cost is non-negative for positive arguments, and the canonical threshold is positive.
Non-negativity ultimately traces to the foundation fact that every recognition-event cost is non-negative (via $J$-cost non-negativity).
proof idea
One-line structure construction. The three fields of the certificate are filled directly by the sibling lemmas: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further tactics or algebraic work.
why it matters
Exports the well-formedness witness for Chemistry Module 10 (laminar CH4 flame speed). The module's MATCH claim $\phi^{-2}\approx 0.40$ m/s sits on top of this certificate; without diagonal vanishing, non-negativity, and a positive threshold, the cost interface would not be a valid recognition-cost statement. No downstream consumers are wired in the current graph; this is the module-local export. It does not itself invoke the forcing chain (T5–T8) or the RCL, but inherits cost non-negativity from the foundation J-cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.