cert
plain-language theorem explainer
Packages three already-proved Materials-domain facts (vanishing self-cost, nonnegativity of domain cost, positive canonical threshold) into the rung-53 structural certificate. Anyone citing the Materials structural prediction at recognition rung 53 uses this bundle. Construction is a pure structure instance: three field assignments, no extra argument.
Claim. There is a structural Materials certificate at recognition rung 53: for every nonzero real $r$, the domain cost satisfies $\mathrm{cost}(r,r)=0$; for all positive $m,e$, $\mathrm{cost}(m,e)\ge 0$; and the canonical threshold is strictly positive.
background
The module states a structural Recognition Science prediction for the Materials domain at recognition rung 53 (Plan v7, 120th pass), with status structural theorem: zero sorry, zero axiom. The certificate is a three-field structure: diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold.
Domain cost is the Materials-side cost functional (imported from the Cost layer and Constants). Nonnegativity of recognition cost is the upstream fact that every recognition event has nonnegative J-cost, via $J(x)=(x+x^{-1})/2-1$ minimized at the identity $x=1$. The local siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields; this definition only packages them.
proof idea
One-line structure instance. The three fields of the Materials rung-53 certificate are filled by the sibling lemmas: diagonal vanishing by the domain-cost-at-equality fact, nonnegativity by the domain-cost nonnegativity lemma (itself resting on the foundation cost-nonnegativity theorem for recognition events), and threshold positivity by the canonical-threshold positivity lemma. No further rewriting or case analysis.
why it matters
This is the inhabiting witness for the Materials structural certificate at rung 53. The module frames it as a structural RS prediction in the Materials domain: cost geometry (zero on matched arguments, nonnegative off-diagonal) plus a positive decision threshold. It sits downstream of the foundation cost-nonnegativity result (J-cost of any recognition event is nonnegative) and upstream of any consumer that needs an inhabited Materials certificate rather than three separate lemmas. No used_by edges are recorded yet; the sibling cert_inhabited is the natural next step. Framework landmarks touched only indirectly: J-uniqueness (T5) and the cost layer that feeds mass and materials ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.