cert
plain-language theorem explainer
Packages three elementary facts about the elastic-modulus domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Anyone assembling an ElasticMod4 witness cites this bundle. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
The module derives a structural elastic-modulus scale from the phi-ladder (Plan v7, 119th pass). Empirically steel sits near $E \sim 200$ GPa; the RS estimate is $\phi^{10}\cdot 2,\mathrm{GPa}\approx 246$ GPa, treated as order-of-magnitude consistent. Status is structural: zero sorry, zero axiom.
The domain cost is the local cost functional on mass/energy pairs used to mark the elastic threshold. The certificate structure demands three properties of that cost and of the canonical threshold: diagonal vanishing, nonnegativity on the positive quadrant, and positivity of the threshold. Upstream, the foundation cost of any recognition event is already known to be nonnegative via the J-cost minimum at identity.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No further rewriting or case analysis occurs.
why it matters
Gives a single inhabited certificate object for the elastic-modulus v4 layer, so downstream physics modules can assume the domain-cost hygiene facts without re-proving them. It sits inside the phi-ladder mass/scale story (primer mass formula and T6 phi fixed point), where $\phi^{10}$ supplies the dimensionless rung that converts a 2 GPa base into the steel-scale modulus. No used-by edges are recorded yet; the immediate consumer is the sibling inhabitedness lemma that witnesses the certificate type is nonempty. Closes no open forcing-chain step (T0–T8), but keeps the elastic-modulus structural theorem free of local sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.