cert
plain-language theorem explainer
Packages the three structural properties of the materials-domain cost used for the steel Young modulus match: diagonal vanishing, non-negativity on positive arguments, and a positive canonical threshold. Anyone citing the Module-1 materials certificate as an inhabited witness uses this value. It is a pure structure assembly wiring three already-proved lemmas.
Claim. A materials Module-1 certificate exists: for every $r\neq 0$, the domain cost at $(r,r)$ is zero; for all $m>0$ and $e>0$, the domain cost at $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Materials RS Module 1 targets steel Young's modulus on the phi-ladder: $\phi^{25}$ MPa equals $196,000$ MPa ($196$ GPa), matching the empirical $\sim 200$ GPa scale. The module is marked a structural theorem (no sorry, no axioms).
The domain cost is the local cost functional on material parameters (modulus and related scales). Its certificate structure demands three facts: the cost vanishes when the two arguments agree and are nonzero; the cost is nonnegative for positive arguments; and a fixed positive threshold (the acceptance cutoff for the match) is available.
Upstream, non-negativity of recognition cost is already forced in the observer layer: every recognition event has cost $\ge 0$ via the J-cost minimum at identity. The materials lemmas specialize that pattern to the domain cost and the module threshold.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of the domain cost, non-negativity of the domain cost on positive pairs, and positivity of the canonical threshold. No new arithmetic is performed.
why it matters
This value is the inhabited witness that Module 1's structural obligations hold, so the steel Young-modulus match sits on a fully discharged certificate rather than an open interface. In the Recognition framework it ties a macroscopic materials constant to the same J-cost and phi-ladder machinery used for particle masses and the forcing chain (T5 J-uniqueness, T6 phi fixed point). Downstream use is currently empty in the graph, but the sibling inhabitedness lemma and any materials aggregator that requires an RSMatl001Cert instance are the natural consumers. It closes the certificate side of a zero-sorry materials claim rather than leaving a hypothesis interface open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.