RSMATStructural004Cert
plain-language theorem explainer
A certificate packing three structural facts for materials gap-45: the domain cost vanishes on the diagonal, stays non-negative off it for positive arguments, and the canonical threshold is strictly positive. Materials and ladder auditors cite it when discharging the minimum stable self-reference rung at D=3 (gap 45). It is a pure structure definition; inhabitance is supplied by the sibling cert bundle.
Claim. A certificate is a triple of properties: (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; (iii) the canonical threshold is strictly positive.
background
Module RS_MAT_Structural_004 treats the materials-side structural claim tied to RS gap-45. At spatial dimension $D=3$ one has $D^2(D+2)=9\cdot 5=45$, identified as the minimum rung for stable self-reference. Status is structural: zero sorry, zero axiom.
The domain cost is the materials-facing cost functional on pairs of positive reals (imported Cost/Constants infrastructure). Its diagonal vanishing and off-diagonal nonnegativity mirror the global J-cost nonnegativity fact from ObserverForcing: "The cost of any recognition event is non-negative." The canonical threshold is the positive cutoff used to separate stable from unstable self-reference on that rung.
The structure does not prove those three facts; it only names the Prop bundle that a later inhabitant must fill.
proof idea
No proof body: this is a structure declaration packing three fields. Inhabitance is deferred to the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos fieldwise, and to cert_inhabited, which wraps that inhabitant as Nonempty. Upstream cost_nonneg supplies the conceptual template (J-cost nonnegativity) that the domain-cost nonnegativity field echoes.
why it matters
Gap-45 is the materials landmark for the lowest rung at which self-reference can stabilize in $D=3$, consistent with the forcing-chain endpoint T8 (three spatial dimensions) and the eight-tick octave T7. Packaging the three cost/threshold obligations as a single certificate lets downstream materials lemmas demand one object rather than three loose hypotheses.
Parents in-module are the concrete inhabitant cert and the nonemptiness theorem cert_inhabited. Together they close the structural side of RS_MAT_Structural_004 with no sorry. The certificate does not itself compute masses or coupling constants; it only locks the cost geometry that those later formulas assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.