cert
plain-language theorem explainer
Packages a three-field certificate that the steel Young-modulus domain cost vanishes on the diagonal, stays non-negative for positive mass/energy arguments, and that the canonical threshold is positive. Materials and RS-constants workers cite it as the inhabited witness for the phi^25 ~ 200 GPa match. The body is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive. Together these witness the RS steel Young-modulus claim ($E\sim\varphi^{25}\,\mathrm{GPa}\approx 196\,\mathrm{GPa}$).
background
Recognition Science matches bulk material constants to integer powers of the golden ratio $\varphi$ on a fixed ladder. For steel, the measured Young modulus is about $200,\mathrm{GPa}$; the module records $\varphi^{25}\approx 1.96\times 10^{5},\mathrm{MPa}=196,\mathrm{GPa}$ as the structural match.
The local certificate structure demands three analytic properties of a domain cost: it is zero when the two arguments coincide (off zero), it is non-negative for positive arguments, and a canonical positive threshold exists. Upstream, the foundation cost $J$ is already known to be non-negative on recognition events (cost_nonneg: "The cost of any recognition event is non-negative"), which underwrites the domain-level non-negativity field.
Sibling lemmas in the same module discharge each field: diagonal vanishing, non-negativity, and positivity of the threshold. The present definition simply assembles those three facts into one inhabited certificate value.
proof idea
One-line structure construction. The three fields of YoungModSteelCert are filled by the in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or tactics; the definition is pure packaging of already-proved sibling facts. The upstream foundation result cost_nonneg (J-cost non-negative on recognition events) is the conceptual ancestor of the domain non-negativity field.
why it matters
Gives the inhabited witness that the steel Young-modulus module is a structural theorem (module status: 0 sorry, 0 axiom). Downstream the sibling cert_inhabited and any materials audit that requires a YoungModSteelCert value depend on this package. In the broader RS ladder it anchors the materials claim $E_{\mathrm{steel}}\sim\varphi^{25},\mathrm{GPa}$ next to the forced constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$) and the T5/T6 J-uniqueness and $\varphi$-fixed-point steps. It does not itself re-derive the numerical $\varphi^{25}$ evaluation; it certifies the cost-theoretic side conditions that make the match admissible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.