RSMATStructural003Cert
plain-language theorem explainer
Certificate type for Materials Structural Module 3: domain cost vanishes on equal nonzero arguments, is nonnegative for positive mass/energy, and the canonical threshold is strictly positive. Cited by anyone assembling or discharging the RS materials count-law interface (seven channels from D=3). Pure structure definition; inhabitants are filled by sibling lemmas, not proved here.
Claim. A materials structural certificate is a triple of facts: for every real $r \neq 0$, the domain cost at $(r,r)$ equals $0$; for all reals $m>0$ and $e>0$, the domain cost at $(m,e)$ is $\ge 0$; and the canonical threshold is strictly positive.
background
This module packages the RS materials count law: with spatial dimension $D=3$ forced upstream, one has $2^D-1=7$ independent channels. Status is structural (no sorry, no axioms). The local cost object is a real bivariate domain cost on mass/energy-like arguments; the canonical threshold is a fixed positive real used as a materials cutoff.
Upstream, recognition cost is already known to be nonnegative: any recognition event has cost $\ge 0$ via the $J$-cost nonnegativity lemma in ObserverForcing. The present certificate lifts that style of bound into a materials-facing interface, requiring diagonal vanishing (equal arguments cost nothing), positivity of the threshold, and nonnegativity off the diagonal for positive inputs.
Sibling lemmas in the same file supply the three field proofs (domainCost on the diagonal, nonnegativity, and threshold positivity); this declaration only names the bundle.
proof idea
No proof body: this is a structure whose three fields are propositions. Field one demands domain cost of $(r,r)$ is zero for $r\neq 0$. Field two demands nonnegativity of domain cost on the positive quadrant. Field three demands the canonical threshold is positive. Downstream cert fills the fields by applying the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that witness as Nonempty.
why it matters
Gives the typed interface for Materials RS Structural Module 3, whose module claim is the count law $2^D-1=7$ independent channels from the $D=3$ configuration dimension (framework landmark T8). Downstream, cert inhabits the structure and cert_inhabited records nonemptiness, so later materials results can depend on a single certificate rather than three scattered lemmas.
The cost fields echo the global recognition-cost nonnegativity story (ObserverForcing / $J$-cost minimum at identity) inside a materials domain. The threshold field anchors any later cutoff or selection rule that needs a strictly positive RS-native scale. No open scaffold remains in this module: the certificate is definitional, and inhabitation is already discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.