ElasticMod4Cert
plain-language theorem explainer
Certificate packing three structural facts for the elastic-modulus-from-phi-ladder story: diagonal domain cost vanishes off zero, domain cost is nonnegative on positive mass and strain, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and a Nonempty proof from it. Pure structure definition with no proof body.
Claim. An elastic-modulus certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all reals $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module ElasticMod4 treats Young's modulus as a phi-ladder quantity. The module note records the RS estimate $\varphi^{10}\cdot 2,\mathrm{GPa}\approx 246,\mathrm{GPa}$ against steel near $200,\mathrm{GPa}$, and marks the development as a structural theorem (no sorry, no axiom).
The certificate refers to a domain cost on pairs of reals (mass-like and strain-like arguments) and to a fixed positive canonical threshold used as a comparison scale. Nonnegativity of recognition cost is the ambient prior: upstream, any recognition event has nonnegative cost via the J-cost minimum at identity.
Local siblings supply the concrete domain-cost diagonal identity, its nonnegativity on the positive quadrant, and positivity of the threshold; the structure only names the interface those lemmas must fill.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on positive arguments, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which assigns the corresponding proved lemmas fieldwise.
why it matters
Gives a single named bundle for the elastic-modulus v4 interface so later physics lemmas can depend on one certificate rather than three scattered hypotheses. Downstream, cert fills the fields from domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited records Nonempty of the structure.
In the broader RS picture this sits under the phi-ladder mass and scale story (T6 fixed point $\varphi$, rung powers such as $\varphi^{10}$), tying a continuum elastic scale to the same cost calculus whose nonnegativity is forced upstream. It does not itself close the numerical steel comparison; it only packages the cost and threshold facts the modulus argument needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.