cert
plain-language theorem explainer
Packages three domain-cost facts into the structural certificate for RS gap-45 (minimum rung 45 for stable self-reference at D=3). Anyone citing the Standard Model structural layer uses this as the inhabited witness. The body is a pure structure instance: it wires equality-at-equal-args, nonnegativity, and positive threshold lemmas into the certificate fields.
Claim. There is a certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of $(r,r)$ vanishes; (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_STD_Structural_004 records the structural gap-45 fact: at spatial dimension $D=3$, the combination $D^2(D+2)=9\cdot 5=45$ is the minimum rung for stable self-reference. The module is marked structural (zero sorry, zero axiom).
The certificate type bundles three properties of a real-valued domain cost on pairs $(m,e)$: vanishing on the diagonal away from zero, nonnegativity for positive arguments, and positivity of a fixed canonical threshold. Upstream, the foundation cost law already guarantees that every recognition event has nonnegative J-cost (the cost of any recognition event is non-negative), which the domain-cost nonnegativity lemma mirrors in this Standard Model setting.
proof idea
One-line structure instance. The three certificate fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs.
why it matters
Gives an inhabited structural certificate for the gap-45 rung that the Standard Model layer treats as the minimum for stable self-reference at $D=3$ (forcing-chain landmark T8). Downstream consumers can take the certificate as a single hypothesis rather than three separate facts. No used-by edges are recorded yet; the companion cert_inhabited sibling is the natural next citation point. Closes the structural packaging step for this module without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.