cert
plain-language theorem explainer
Packages three elementary facts about the green-chemistry domain cost into a single certificate: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone working the structural count of Anastas's twelve principles in RS units would cite this bundle. The body is a pure structure constructor that wires three already-proved sibling lemmas.
Claim. There exists a green-chemistry principles certificate: for every nonzero real $r$, the domain cost at $(r,r)$ is zero; for all positive measure $m$ and effort $e$, the domain cost is nonnegative; and the canonical threshold is strictly positive.
background
The module treats Anastas's twelve green-chemistry principles as a structural count inside Recognition Science. The module doc records the candidate identities $12 = 2^D-1+D+1$ (with $D=3$) and $12 = 4\cdot\mathrm{configDim}$, and notes the numerical coincidence $12\approx\varphi^5$. Status is a structural theorem with zero sorry and zero axioms.
The certificate structure bundles three cost axioms for a domain cost on pairs of reals (measure and effort). The first axiom is a diagonal vanishing law: equal nonzero arguments cost nothing. The second is nonnegativity on the positive quadrant. The third asserts that a fixed positive threshold (the canonical cutoff used by the metrics) is strictly positive. Upstream, the foundation lemma cost_nonneg already guarantees that every recognition-event cost is nonnegative via the J-cost $J(x)=(x+x^{-1})/2-1$.
proof idea
Pure structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional rewriting or case analysis occurs; the definition is the witness that those three facts inhabit the certificate type.
why it matters
Gives a single named inhabitant of the green-chemistry principles certificate, so downstream chemistry metrics can assume the cost axioms by name rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity. It sits inside the structural program that ties Anastas's twelve principles to the RS dimension count $D=3$ (forcing chain T8) and to the eight-tick / config-dimension arithmetic. No downstream theorems yet depend on it (used_by is empty), but the sibling cert_inhabited and any future green-metrics theorems are the natural consumers. It does not itself derive the twelve named Anastas principles; it only certifies the cost infrastructure those metrics rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.