cert
plain-language theorem explainer
Packages three structural facts about the dielectric-water domain cost into one certificate: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Chemists or RS auditors citing Module 12 (water dielectric, φ⁹ ≈ 76 vs ~78.5) would reference this bundle. Construction is a pure structure assembly of three already-proved lemmas.
Claim. There is a certificate recording that the dielectric-water domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
Chemistry RS Module 12 treats dielectric water as a structural theorem: the RS prediction $\varphi^9\approx 76.0$ sits about 3% from the experimental dielectric constant $\sim 78.5$. The module is marked structural (zero sorry, zero axiom).
The domain cost is the local cost functional on mass/energy pairs used to score recognition events in this chemistry setting. It inherits the global J-cost nonnegativity from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative), specialized here to positive real arguments. The canonical threshold is the positive cutoff against which that cost is compared.
RSChem012Cert is the structure that packages the three required properties: diagonal vanishing of the domain cost, its nonnegativity on the positive quadrant, and positivity of the threshold.
proof idea
Pure structure construction. The three fields of RSChem012Cert are filled by the sibling lemmas domainCost_at_eq (diagonal identity), domainCost_nonneg (nonnegativity on positive reals), and canonicalThreshold_pos (threshold positivity). No extra algebra; the definition is the certificate instance itself.
why it matters
Gives the single named certificate that Module 12 is structurally sound: the water-dielectric domain cost behaves like a genuine recognition cost (zero on matched pairs, nonnegative, with a positive decision threshold). That matches the module status line STRUCTURAL THEOREM and the φ-ladder landmark φ⁹ for the dielectric scale. No downstream users are recorded yet; the natural consumer is any chemistry-layer theorem that needs a discharged RSChem012Cert hypothesis, or the sibling cert_inhabited inhabitation proof. Does not close the 3% numerical gap to experiment; it only certifies the cost axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.