RSMatl007Cert
plain-language theorem explainer
Certificate bundle for Materials module 7 (power-law creep with exponent n = D = 3). It packages three structural facts: the domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance to treat the module as certified. The structure itself is pure data; the proofs live in the field fillers.
Claim. A certificate for the creep module consists of three properties of the materials domain cost $C$ and threshold $\tau$: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
Materials RS Module 7 asserts that the power-law creep exponent equals spatial dimension: $n=D=3$, forced exactly (structural theorem, no sorry or axiom). The local cost is a domain-specific specialization of the Recognition J-cost, imported from the Cost layer and Constants.
Upstream, ObserverForcing records that every recognition event has non-negative cost via $J$-cost non-negativity on positive states. The module lifts that idea to a two-argument materials cost $C(m,e)$ together with a positive canonical threshold used as a comparison scale.
The certificate structure does not itself prove the creep law. It only freezes the three numerical/inequality side conditions the rest of the module treats as the certified interface.
proof idea
No proof body: this is a structure declaration. Inhabitation is supplied downstream by cert, which fills the three fields with the sibling lemmas that establish diagonal vanishing of the domain cost, non-negativity for positive mass/energy arguments, and positivity of the canonical threshold. cert_inhabited is then the one-line Nonempty witness ⟨cert⟩.
why it matters
Gives the module a single named inhabitable type that downstream materials proofs can require instead of re-proving cost hygiene. Parent uses are the concrete certificate value and the Nonempty theorem that marks the module certified.
In the broader RS chain this sits under the $D=3$ forcing (T8) and the eight-tick / octave geometry that fix the creep exponent as exactly three. The cost fields echo the global J-cost minimum and non-negativity that begin at T5 and the Recognition Composition Law. The module claims an exact structural identification $n=D=3$ rather than a fit parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.