cert
plain-language theorem explainer
Packages the three structural side-conditions for Chemistry Module 4 (acetic pKa) into a single certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the acetic-acid pKa match (φ³·1.124 = 4.76) uses this bundle. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Chemistry RS Module 4 records the acetic-acid pKa match $\phi^3 \cdot 1.124 = 4.76$ as a structural theorem (zero sorry, zero axiom). The local cost is the usual Recognition Science J-cost pulled into a two-argument domain cost on positive reals: it measures mismatch between a measured value and an expected ladder value.
The certificate structure RSChem004Cert is the module's interface contract. It demands three elementary properties of that cost and of the module's canonical threshold: diagonal vanishing (perfect match costs nothing), nonnegativity (no negative recognition cost), and a positive decision threshold. Upstream, nonnegativity of recognition cost is the standard fact that $J$-cost is nonnegative on positive states (ObserverForcing / Cost).
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra is performed at this site; the definition only assembles already-proved facts into the certificate type.
why it matters
Gives Module 4 a single named inhabitant of its structural certificate, so downstream chemistry or audit code can depend on one object rather than three separate lemmas. The module doc frames the scientific claim as the acetic pKa identity $\phi^3 \cdot 1.124 = 4.76$ under the RS phi-ladder; this certificate is the cost-side hygiene that makes that match well-typed as a recognition event (cost zero on match, nonnegative otherwise, positive threshold). No further used-by edges are recorded yet; the declaration is the module's exportable proof package. It sits under the broader RS cost calculus (J-uniqueness / T5, RCL) rather than under mass or alpha forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.