cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single kinetic-resolution certificate at the phi^3 scale. Chemists or RS auditors cite it when they need a ready witness that the J-cost on matched rates vanishes, stays nonnegative off-diagonal, and sits under a positive threshold. The body is a pure structure assembly: three preexisting lemmas fill the three fields.
Claim. There is a kinetic-resolution certificate asserting: (i) the domain cost of any nonzero rate against itself is zero; (ii) for positive matched and excess rates the domain cost is nonnegative; (iii) the canonical selectivity threshold is strictly positive.
background
The module treats asymmetric kinetic resolution in Recognition Science units. Selectivity is the ratio $s = k_{\mathrm{fast}}/k_{\mathrm{slow}}$; RS forces $s = \varphi^n$ at $n$ recognition rungs of energy difference, so $\varphi^3 \approx 4.24$ and $\varphi^5 \approx 11$ mark the practical bands (empirical good resolution often wants $s > 10$--$50$).
Domain cost is the J-cost specialized to a pair of positive real rates (matched vs excess). The J-cost itself is the unique nonnegative cost forced by the Recognition Composition Law, minimized at identity and nonnegative everywhere (upstream cost_nonneg: "The cost of any recognition event is non-negative"). The certificate structure simply records the three algebraic properties needed before any selectivity comparison is stated.
proof idea
One-line structure construction. The three fields of KinRes3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No new arithmetic is performed; the definition is pure packaging.
why it matters
Gives the module a single named witness that the J-cost side of kinetic resolution is well-formed before any claim about $\varphi^3$ selectivity is made. The module status line calls the surrounding development a structural theorem (0 sorry, 0 axiom). Downstream use is presently empty in the graph, so the certificate is the local anchor for later selectivity or inhabitation lemmas (e.g. the sibling inhabitation fact). It sits inside the chemistry layer that imports only Constants and Cost, keeping the link to the forced J-cost (T5) and the phi ladder explicit and minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.