cert
plain-language theorem explainer
Packages three elementary properties of the ethanol-boiling domain cost into a single certificate: diagonal vanishing, non-negativity, and a positive canonical threshold. Anyone citing the RS structural match of ethanol's boiling point to the phi ladder uses this inhabitant. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There exists a certificate asserting that the ethanol-boiling 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
Recognition Science treats phase-change temperatures as recognition events whose cost is measured by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). In this module the domain cost is the specialization of that cost to the ethanol boiling regime; the canonical threshold is the positive scale against which the match is judged.
The module records the empirical match: ethanol boils at $351,\mathrm{K}$, recovered as $\phi^7\cdot 12.1,\mathrm{K}$. The certificate structure simply freezes the three algebraic properties any such cost must obey before the numerical comparison is meaningful.
Upstream, non-negativity of recognition cost is already proved for general recognition events via $J$-cost non-negativity; the local lemmas domainCost_nonneg and domainCost_at_eq are the chemistry-side specializations.
proof idea
Pure structure inhabitant. The three fields of EthanolBoilingCert are filled by the three already-proved sibling facts: diagonal vanishing (domainCost_at_eq), non-negativity on the positive quadrant (domainCost_nonneg), and positivity of the canonical threshold (canonicalThreshold_pos). No additional tactics or arithmetic are required.
why it matters
Gives a zero-sorry, zero-axiom certificate that the ethanol boiling cost is a legitimate RS cost functional. The module presents this as a structural theorem supporting the numerical claim $\phi^7\cdot 12.1,\mathrm{K}=351,\mathrm{K}$. Downstream consumers (none yet recorded) can treat the three cost axioms as a single inhabited package rather than re-proving them. It sits in the chemistry layer that applies the forcing-chain constants ($\phi$ from T6, J-uniqueness from T5) to concrete molecular scales; it does not itself advance T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.