cert
plain-language theorem explainer
Packages the three structural hypotheses of the Eyring-from-φ-ladder certificate: domain cost vanishes on the equilibrium diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the structural Eyring rate theorem in this chemistry module uses this witness. It is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is an Eyring-rate certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(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
The module develops Eyring transition-state theory inside Recognition Science. Classically $k = (kT/h) K^\ddagger$ with $K^\ddagger = \exp(-\Delta G^\ddagger/RT)$. RS identifies the barrier with the J-cost of the golden ratio at the recognition transition state, so the canonical rate at $T_c$ is $k = (kT/h)\exp(-J(\varphi)) \approx (kT/h)\times 0.889$.
Domain cost is the local cost functional on reactant/product (or mass/energy) pairs used to model that barrier. The certificate structure demands three facts: cost vanishes when the two arguments coincide (equilibrium), cost is nonnegative off that diagonal for positive inputs, and a fixed positive threshold (the canonical recognition threshold) exists.
Upstream, nonnegativity of recognition cost is the standard J-cost fact: every recognition event has cost $\ge 0$, since $J$ is nonnegative on positive reals.
proof idea
One-line structure instance. The three fields of EyringRateCert are filled by the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work; the definition is just the witness record.
why it matters
Gives a single inhabited certificate object for the structural Eyring-rate development in the chemistry layer (Plan v7, eighty-fourth pass). Downstream consumers can take the whole package rather than re-proving equilibrium vanishing, nonnegativity, and threshold positivity separately. It sits under the RS reading of TST in which $\Delta G^\ddagger$ is $J(\varphi),RT_c$, tying the rate prefactor to the T5/T6 J-uniqueness and $\varphi$-fixed-point landmarks. No used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer. Status is structural (0 sorry, 0 axiom), so this closes the certificate interface rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.