cert
plain-language theorem explainer
Packages three elementary properties of the materials domain cost into a single certificate: vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Materials theorists linking Taylor hardening to the RS J-cost would cite it as the structural witness. The body is a three-field structure instance wiring preexisting lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero ratio $r$ against itself vanishes, $\mathrm{cost}(r,r)=0$; (ii) for all positive $m,e$, the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats Taylor hardening $\sigma_{\mathrm{flow}} = \alpha G b \sqrt{\rho}$ in Recognition Science units. The RS claim is that the dimensionless prefactor is the J-cost at the golden ratio, $\alpha = J(\varphi) \approx 0.118$ (empirical FCC range $\approx 0.1$–$0.5$), and that at hardening saturation one has $\rho b^2 = J(\varphi)$.
Domain cost is the materials-side specialization of the recognition cost $J$, imported from the Cost layer. The structure DislocationCert packages the three minimal analytic properties needed before any density or hardening identity is stated: equilibrium vanishing, nonnegativity, and a positive threshold scale.
Upstream, nonnegativity of recognition cost is already forced (cost_nonneg: the cost of any recognition event is non-negative), so the materials nonnegativity field is the corresponding specialization rather than a new analytic fact.
proof idea
Three-field structure instance, not a tactic proof. Each field is filled by a named sibling lemma already proved in the module: equilibrium vanishing by domainCost_at_equilibrium, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives the materials module a single named witness that the domain-cost side of the dislocation story is well-posed before any saturation or density identity is invoked. The module status line marks the whole development as a structural theorem (zero sorry, zero axiom), and this certificate is the entry point for that claim.
It sits under the broader RS forcing chain only indirectly: the cost $J$ is the unique T5 solution of the Recognition Composition Law, and $\varphi$ is the T6 fixed point, so identifying $\alpha = J(\varphi)$ and $\rho b^2 = J(\varphi)$ at saturation is a materials-level reading of those landmarks rather than a new forcing step. No downstream consumers are wired yet; the sibling inhabitedness fact is the immediate companion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.