RSMatl006Cert
plain-language theorem explainer
Certificate bundle for Materials module 6 (water specific heat). It packages three structural facts: the domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is strictly positive. Downstream code builds an inhabited instance from the sibling lemmas. Pure structure definition; no proof obligations live here.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T_*$ obeys $T_*>0$.
background
Module 6 targets the water specific-heat match $c_p \approx \varphi^{19}\cdot 0.447,\mathrm{J/kg/K}\approx 4179,\mathrm{J/kg/K}$ (reported exact to $0.01%$). Status is structural: zero sorry, zero axioms.
The domain cost $C(m,e)$ is the materials-side cost functional on mass/energy coordinates (sibling domainCost). The diagonal vanishing and nonnegativity clauses mirror the global J-cost geometry: Recognition cost is nonnegative, and the identity event sits at the J-minimum. Upstream, cost_nonneg states that every recognition event has nonnegative cost via Jcost_nonneg.
canonicalThreshold is the positive cutoff used to gate the materials claim; its positivity is one of the three fields packed here.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued hypotheses naming the diagonal identity, nonnegativity, and threshold positivity. Inhabitation is discharged downstream by cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the structural side-conditions of the water $c_p$ module so that cert and cert_inhabited can export a clean Nonempty witness. That pattern keeps the materials ledger uniform: each RS_Matl module ships a certificate packing cost geometry plus threshold positivity, then proves the certificate is inhabited.
Framework link is indirect but real: nonnegativity and diagonal vanishing are the materials shadow of T5 J-uniqueness and the RCL cost law ($J(x)=(x+x^{-1})/2-1$), while the $\varphi$-ladder supplies the numerical rung for $c_p$. The certificate does not itself compute $4179$; it only locks the cost/threshold scaffolding the module claims as structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.