cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the Module-7 materials certificate: cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the structural claim that the creep exponent equals spatial dimension three will need this bundle. The definition is a pure structure assembly of three sibling lemmas already proved in-module.
Claim. There is a certificate recording that the materials 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
Module 7 of the RS materials layer targets power-law creep with exponent $n=D=3$, treated as an exact structural identity (zero sorry, zero axiom). The local cost is a two-argument domain cost $C(m,e)$ built from the Recognition J-cost; the certificate structure simply freezes the three inequalities any downstream materials argument is allowed to assume about $C$ and the threshold.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals. The in-module siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that fact to the materials cost and record that the chosen threshold sits strictly above zero.
The certificate type is the interface object: three fields, no extra data. Filling it is the only content of this definition.
proof idea
One-line structure constructor. The three fields of the certificate are assigned the three already-proved sibling lemmas: diagonal vanishing, nonnegativity for positive mass/energy arguments, and positivity of the canonical threshold. No new algebra is performed here.
why it matters
This is the inhabitation witness for the Module-7 materials certificate. The module claims the creep exponent equals spatial dimension three as an exact structural theorem; the certificate packages the cost and threshold side-conditions that any such argument must carry. It sits downstream of the global J-cost nonnegativity fact and of the forcing-chain landmark $D=3$ (T8). No further consumers are wired in the present graph, so the definition mainly closes the local interface rather than feeding a named parent theorem yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.