cert
plain-language theorem explainer
Packages three structural facts about the freezing-point domain cost into one certificate: diagonal vanishing, nonnegativity for positive mass and energy, and a positive canonical threshold. Chemists or RS auditors citing the FP-depression v4 model use this bundle rather than the three lemmas separately. The body is a pure structure instance that wires three sibling proofs.
Claim. There is a certificate asserting: (i) the domain cost of equal nonzero arguments vanishes, $\mathrm{cost}(r,r)=0$ for $r\neq 0$; (ii) for positive mass $m$ and energy $e$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Module FPDepression4 treats freezing-point depression as a structural consequence of the Recognition Science J-cost, not a fitted cryoscopic constant. The module note records the empirical water value $K_f\approx 1.853$ and contrasts naive phi-ladder guesses ($\phi+J(\phi)$, $\phi^{-1}$) against a purely structural claim with zero sorry and zero axioms.
The certificate structure bundles three properties of a real bivariate domain cost: it is zero on the diagonal away from zero, nonnegative on the positive quadrant, and compared against a positive canonical threshold. Nonnegativity of recognition cost is the ambient fact from ObserverForcing: every recognition event has cost $\ge 0$ because $J$ is nonnegative on positive reals.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields; this definition only assembles them.
proof idea
One-line structure instance. Field cost_at_eq is filled by the sibling lemma that the domain cost vanishes when both arguments equal a nonzero real. Field cost_nonneg is filled by the sibling nonnegativity lemma on positive mass and energy (itself resting on the foundation fact that J-cost is nonnegative). Field threshold_pos is filled by the sibling proof that the canonical threshold is positive. No extra tactics or rewriting.
why it matters
Gives a single named inhabitant of the FP-depression v4 certificate so downstream chemistry developments can assume the three structural axioms as one object rather than three separate hypotheses. The module frames this as a structural theorem in the J-cost freezing-point program (Plan v7, 119th pass), distinct from numerical matching of water's $K_f$. No used-by edges are recorded yet; the natural consumer is any lemma that needs a packaged proof that the domain cost is a genuine nonnegative cost with a positive threshold, in the same spirit as the foundation cost-nonnegativity result. Touches the broader RS theme that macroscopic thermodynamic shifts should reduce to properties of $J$ and the phi ladder rather than free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.