YieldStrengthCert
plain-language theorem explainer
A certificate structure bundling three positivity and equilibrium axioms for the domain cost used in φ-ladder yield-strength scaling. Materials theorists cite it when packaging Hall–Petch-type grain-size strengthening σ_y ∝ d^{-φ/4} as a checked Lean object. It is a pure structure definition: three Prop fields, no proof body. Downstream code inhabits it once and proves non-emptiness.
Claim. A yield-strength certificate is a triple of properties: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments, $0<m,\,0<e\Rightarrow C(m,e)\ge 0$; (iii) the canonical threshold $T_*$ is strictly positive, $T_*>0$.
background
The module develops yield-strength scaling from the Recognition Science φ-ladder (Plan v7). The stated materials law is Hall–Petch grain-size strengthening written with the golden-ratio exponent: $\sigma_y \propto d^{-\varphi/4}$ across metals. Status is structural: zero sorry, zero axiom.
Domain cost $C(m,e)$ is the local cost functional on mass/energy-like coordinates that the yield model uses in place of a raw J-cost. Equilibrium means equal nonzero arguments; the certificate demands $C(r,r)=0$ there. Nonnegativity for positive arguments mirrors the foundation fact that recognition-event cost is nonnegative (ObserverForcing: cost of any recognition event satisfies $0\le e.\mathrm{cost}$, via $J$-cost nonnegativity).
The canonical threshold $T_$ is the positive scale against which domain cost is compared when a grain or defect configuration is declared to have yielded. The certificate only records $T_>0$; the numerical φ-ladder value lives in sibling definitions.
proof idea
No proof body: this is a structure declaration. The three fields are bare propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line non-emptiness theorem that wraps that instance.
why it matters
The certificate is the typed interface for the materials yield-strength layer. Downstream, a single canonical instance is built and Nonempty is proved, so later lemmas can assume a certificate rather than restate the three axioms. That keeps the Hall–Petch φ-ladder claim modular: equilibrium vanishing, cost positivity, and a positive threshold are the only structural inputs.
In the broader framework this sits under materials phenomenology fed by the φ-ladder and the nonnegative J-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). It does not itself derive $\sigma_y \propto d^{-\varphi/4}$; it packages the cost hypotheses that such a derivation is allowed to use. Parent uses are the canonical certificate instance and the inhabitedness theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.