cert
plain-language theorem explainer
Packages three structural facts about the chemistry domain cost into a single certificate for RS Chemistry Module 1 (water pKw ≈ 14 via φ³). Anyone citing the module's structural status uses this witness. The definition is a pure record assembly: it plugs in the diagonal-vanishing, non-negativity, and positive-threshold lemmas already proved in-module.
Claim. There is a certificate asserting: (i) the chemistry domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
Chemistry RS Module 1 targets the water ion-product identity $\mathrm{p}K_w=14$ as a structural match: $\varphi^3\cdot 3.302\approx 14$ (with $\varphi^3\approx 4.236$). The module is marked structural (zero sorry, zero axiom).
The domain cost $C$ is the local cost functional on chemistry-scale ratios; its diagonal vanishing and non-negativity mirror the global J-cost properties from Recognition Science ($J(x)=(x+x^{-1})/2-1$, minimized at identity). Upstream, cost_nonneg in ObserverForcing states that every recognition event has non-negative cost via $J\ge 0$.
RSChem001Cert is the structure bundling the three Prop fields that a chemistry certificate must supply: diagonal equality to zero, non-negativity on the positive quadrant, and positivity of the canonical threshold.
proof idea
One-line record construction. The three fields of RSChem001Cert are filled by the already-proved in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is performed; the definition is pure packaging of those three facts into a single witness value.
why it matters
Gives the inhabited certificate that Module 1 is structurally closed: the chemistry domain cost behaves like a genuine recognition cost (zero on matched ratios, non-negative off-diagonal) and the threshold used for the $\mathrm{p}K_w$ match is positive. Downstream consumers (none listed yet in the graph) would cite this rather than the three lemmas separately when discharging "Module 1 certified" hypotheses.
In the broader framework it is the chemistry-side analogue of packaging J-cost non-negativity and identity minimum; it does not itself derive $\varphi$ or the eight-tick octave, but it sits under the same cost axioms forced by T5 (J-uniqueness) and the Recognition Composition Law. The module doc's numerical match $\varphi^3\cdot 3.302\approx 14$ is the physical claim this certificate underwrites structurally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.