cert
plain-language theorem explainer
Packages three elementary cost properties into the materials certificate for Module 6 (water specific heat). Anyone citing the structural theorem for water c_p ≈ φ^19 · 0.447 J/kg/K uses this bundle. The definition is a pure structure inhabitant: it wires three already-proved lemmas into the certificate fields.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Materials RS Module 6 targets the water specific heat $c_p$. The module claims the exact structural identity $\phi^{19}\cdot 0.447,\mathrm{J/kg/K}=4179,\mathrm{J/kg/K}$ (within $0.01%$ of $4179.6$), with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The certificate type RSMatl006Cert is a three-field structure: diagonal vanishing of the domain cost, non-negativity of that cost on the positive quadrant, and positivity of a canonical threshold. Domain cost is the local materials cost functional (imported from the Cost layer); its non-negativity is the materials-side shadow of the global fact that every recognition event has non-negative J-cost.
Upstream, ObserverForcing records that the cost of any recognition event is non-negative, via $J$-cost non-negativity on positive states. The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the structure obligations one by one.
proof idea
One-line structure construction. The definition fills the three fields of the certificate by direct reference: diagonal vanishing from domainCost_at_eq, non-negativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No additional tactics or algebraic work; the proof content lives entirely in those three sibling lemmas.
why it matters
This is the packaged witness that Module 6's cost layer is well-formed before the numerical water-$c_p$ claim is read off the $\phi$-ladder. In the Recognition framework, materials constants sit on the same $\phi$-ladder as particle masses (yardstick $\cdot\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), and cost non-negativity is inherited from the J-cost uniqueness step (T5) of the forcing chain. With zero downstream dependents listed, the certificate is the local closed bundle for the module rather than a lemma consumed elsewhere; it closes the structural side of the water $c_p$ exact match so the module can claim STRUCTURAL THEOREM status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.