cert
plain-language theorem explainer
Packages the three structural obligations of the ethanol-boiling chemistry certificate: diagonal vanishing of domain cost, nonnegativity for positive mass/energy, and positivity of the canonical threshold. Anyone citing the RS Chem 011 match (phi^7 * 12.1 K ≈ 351 K) uses this inhabitant. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There exists a certificate recording that (i) the domain cost of any nonzero ratio against itself is zero, (ii) domain cost is nonnegative whenever both arguments are positive, and (iii) the canonical threshold is strictly positive.
background
Module 11 of the RS chemistry layer targets ethanol boiling: the claimed match is $\phi^7 \cdot 12.1,\mathrm{K} = 351,\mathrm{K}$, reported as a structural theorem with no sorry and no axioms. The local cost is a domain-specialized instance of the Recognition Science $J$-cost (the unique nonnegative cost forced by the Recognition Composition Law, with minimum at the identity ratio $x=1$).
The certificate structure RSChem011Cert packages three Prop fields that any valid domain cost must satisfy: vanishing on the diagonal $r\neq 0\Rightarrow C(r,r)=0$, nonnegativity for positive arguments, and a strictly positive canonical threshold. Upstream, the foundation lemma cost_nonneg already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity.
proof idea
One-line structure inhabitant. Each field of the certificate is filled by the corresponding in-module lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the ethanol-boiling domain cost obeys the three structural axioms required of RS chemistry modules. Downstream consumers (none yet wired in the graph) can take this certificate rather than re-proving the three properties. It sits inside the broader phi-ladder mass/temperature matching program: rung exponents built from $\phi$ (the T6 self-similar fixed point) convert dimensionless RS units into kelvin-scale observables. The module status line marks the ethanol match as closed at the structural level; this definition is the packaged proof object for that closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.