cert
plain-language theorem explainer
Canonical inhabited certificate packing three structural facts for yield-strength scaling: domain cost vanishes at equal nonzero arguments, is nonnegative for positive mass/energy, and the canonical threshold is positive. Materials work on Hall-Petch φ-ladder strengthening cites this bundle. Proof is a three-field structure instance wiring existing lemmas.
Claim. There is a yield-strength certificate asserting: (i) the domain cost of any nonzero $r$ against itself is zero; (ii) for positive $m,e$, the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module develops Hall-Petch grain-size strengthening in Recognition Science units, targeting the scaling $\sigma_y \propto d^{-\varphi/4}$ across metals. Domain cost is the local cost functional on a pair of positive real arguments (mass-like and energy-like scales); at equilibrium the two arguments coincide and the cost must sit at its minimum.
The certificate structure YieldStrengthCert packages exactly three obligations: vanishing of domain cost on the diagonal away from zero, nonnegativity off the diagonal for positive inputs, and positivity of a canonical threshold used as the yield cutoff. Upstream, nonnegativity of recognition cost is already forced by the J-cost minimum (cost_nonneg: any recognition event has nonnegative cost, via Jcost_nonneg).
Constants live in RS-native units with $\varphi$ the self-similar fixed point from the forcing chain (T6).
proof idea
One-line structure instance. The three fields of the certificate are filled by named sibling lemmas already proved in-module: domainCost_at_equilibrium supplies diagonal vanishing, domainCost_nonneg supplies nonnegativity for positive arguments, and canonicalThreshold_pos supplies threshold positivity. No extra algebra is performed at this site.
why it matters
Gives a single inhabited witness that the structural side-conditions of the φ-ladder yield-strength story hold. The module frames this as a structural theorem (zero sorry, zero axiom) supporting Hall-Petch scaling $\sigma_y \propto d^{-\varphi/4}$. Downstream edges are not yet wired in the graph, so the certificate presently stands as the local closure point for the three cost/threshold hypotheses rather than a lemma consumed by a named parent theorem. It sits in the materials layer built on the J-cost and $\varphi$-ladder infrastructure (T5–T6 landmarks).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.