RSMTHStructural004Cert
plain-language theorem explainer
Certificate packing three structural facts for the gap-45 module: diagonal domain cost vanishes off zero, domain cost is nonnegative on the positive quadrant, and the canonical threshold is strictly positive. Cited by the module's inhabited certificate and any consumer that needs a single witness of those inequalities. Pure structure definition; no proof body.
Claim. A certificate is a triple of statements: (i) for every nonzero real $r$, the domain cost of $(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_MTH_Structural_004 packages the gap-45 structural claim: at spatial dimension $D=3$, the combination $D^2(D+2)=45$ is the minimum rung supporting stable self-reference. Status is a structural theorem with no sorry and no axioms.
Domain cost is the local cost functional on pairs of positive reals used in this module (siblings domainCost, domainCost_at_eq, domainCost_nonneg). The canonical threshold is the positive cutoff tied to that gap (siblings canonicalThreshold, canonicalThreshold_pos). Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via the J-cost nonnegativity lemma, which is the same positivity pattern this certificate reuses at the domain-cost level.
proof idea
No proof: this is a structure declaration. It only names the three fields that a later inhabitant must supply. The concrete witness is the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. Nonemptiness is then immediate from cert_inhabited.
why it matters
Gives a single typed bundle for the three inequalities the gap-45 structural story needs before it can talk about a positive rung threshold and a well-behaved domain cost. Downstream, cert inhabits the structure and cert_inhabited records Nonempty RSMTHStructural004Cert, so later mathematics modules can assume the certificate rather than re-prove diagonal vanishing, positivity, and threshold positivity. Ties to the forcing-chain landmark $D=3$ (T8) and to the phi-ladder rung counting that places stable self-reference at gap 45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.