DislocationCert
plain-language theorem explainer
A certificate structure packaging three algebraic properties of domain cost for dislocation-density hardening: cost vanishes on the diagonal, cost is nonnegative for positive arguments, and the canonical threshold is positive. Materials theorists linking Taylor hardening to J-cost would cite it. Pure structure definition; no proof body.
Claim. A dislocation certificate is a record of three facts about the domain cost $C$ on pairs of reals and a canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module treats Taylor hardening $\sigma_{\mathrm{flow}}=\alpha G b\sqrt{\rho}$ inside Recognition Science. Empirically $\alpha\sim 0.1$–$0.5$ for FCC metals; RS identifies $\alpha=J(\varphi)\approx 0.118$, and at hardening saturation $\rho b^{2}=J(\varphi)$. Domain cost is the J-cost specialized to a pair of positive material parameters (the local stand-in for recognition mismatch between those scales). The canonical threshold is the positive scale against which that cost is compared when density is read off.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $\ge 0$ via $J$-cost nonnegativity on positive states. The present structure simply names the three Prop fields a materials certificate must carry so that later constructions can inhabit it without re-proving those facts inline.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields by the corresponding lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named bundle for the algebraic hypotheses of the dislocation-density-from-J-cost story, so downstream code can depend on one object rather than three loose lemmas. Immediate consumers are the canonical inhabitant cert and the theorem cert_inhabited establishing Nonempty DislocationCert. In the broader RS chain this sits under T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the forced self-similar scale $\varphi$: the materials reading $\alpha=J(\varphi)$ and $\rho b^{2}=J(\varphi)$ at saturation is only meaningful once cost nonnegativity, equilibrium vanishing, and a positive threshold are packaged. Status is structural (0 sorry, 0 axiom); it does not itself close a forcing step, but it is the interface the materials pass uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.