cert
plain-language theorem explainer
Packages three structural facts about the Diels-Alder endo domain cost into one certificate record: diagonal vanishing, nonnegativity, and a positive canonical threshold. Chemists or RS auditors citing Module 6's endo MATCH claim (1 - J(φ) ≈ 88.2%) would reference this bundle. Construction is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate record asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Chemistry RS Module 6 treats Diels-Alder endo selectivity. The module claims a structural match: $1-J(\varphi)=88.2%$ against the empirical 80-95% band, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The domain cost is the local cost functional on positive real mass/energy-style arguments used in this chemistry layer. It inherits nonnegativity from the global recognition cost $J$, whose nonnegativity is the ObserverForcing fact that every recognition event has cost $\ge 0$ (via $J$-cost nonnegativity at positive state). The canonical threshold is the positive cutoff against which domain-cost comparisons are made in the module.
RSChem006Cert is the structure bundling the three elementary properties required before any selectivity comparison is well-posed: diagonal zero, nonnegativity off-axis, and a positive threshold.
proof idea
One-line structure construction. The three fields of RSChem006Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new arithmetic is performed; the definition is pure packaging. Upstream, nonnegativity of recognition cost (ObserverForcing cost_nonneg, via $J$-cost) underwrites the domain-cost nonnegativity sibling.
why it matters
This certificate is the inhabited witness that Module 6's cost infrastructure is coherent before the endo selectivity MATCH is read off. The module-level claim is the Diels-Alder endo fraction $1-J(\varphi)=88.2%$ inside the empirical 80-95% window, tying chemistry selectivity to the unique $J$-cost forced at T5 and to $\varphi$ at T6.
No downstream consumers are recorded yet (used_by empty). The sibling cert_inhabited is the natural next step that turns this definition into a proof of existence. The declaration closes the structural side of the module (0 sorry, 0 axiom) without itself computing the 88.2% figure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.