cert
plain-language theorem explainer
Packages the three structural facts required by the Module 11 materials certificate: diagonal vanishing of the domain cost, nonnegativity of that cost, and positivity of the canonical threshold. Anyone citing the water specific-heat structural theorem (φ¹⁹·0.447 = 4179 J/kg/K) uses this bundle. The definition is a pure structure inhabitant that wires three already-proved lemmas into the certificate fields.
Claim. The Module 11 materials certificate is the triple of statements: (i) for every $r \neq 0$, the domain cost at $(r,r)$ is zero; (ii) for all $m,e > 0$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Materials RS Module 11 records the exact structural claim that the specific heat of water equals $\phi^{19} \cdot 0.447 = 4179$ J/kg/K, with status structural theorem (zero sorry, zero axiom). The local certificate type collects the cost-theoretic side conditions that underwrite such materials identities.
Domain cost is the module's specialization of the Recognition Science J-cost to a mass/energy pair $(m,e)$. Upstream, the foundation result cost_nonneg states that the cost of any recognition event is nonnegative, via nonnegativity of $J$. The certificate also demands that cost vanish on the diagonal $m = e$ (balanced recognition) and that a positive canonical threshold exist against which the materials identity is scored.
Sibling lemmas already establish each of those three properties for this module's domain cost and threshold; the certificate is their joint packaging.
proof idea
One-line structure construction. The three fields of RSMatl011Cert are filled by the corresponding in-module lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further tactic work; the definition is pure wiring of already-proved facts into the certificate record.
why it matters
Gives a single named inhabitant of the Module 11 certificate type so downstream materials or ledger code can demand "a cert" rather than three separate hypotheses. The module doc frames the target identity as an exact structural theorem for water's specific heat on the $\phi$-ladder ($\phi^{19}$ rung factor). In the broader RS forcing chain this sits downstream of T5 J-uniqueness and the nonnegativity of $J$, which guarantee that balanced recognition sits at cost zero and that off-diagonal costs cannot go negative. No used_by edges are recorded yet; the immediate consumer is the sibling inhabitedness fact and any later materials ledger that indexes Module 11 by certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.