cert
plain-language theorem explainer
Packages three structural facts about the gravity-domain cost and its threshold into a single certificate for RS gap-45 (minimum stable self-reference rung at D=3). Anyone citing the module-4 structural theorem uses this bundle rather than the three lemmas separately. The definition is a pure structure instance: each field is filled by an already-proved sibling lemma.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is non-negative for positive mass and energy arguments; and (iii) the canonical threshold is strictly positive.
background
Module 4 of the RS gravity structural series treats gap-45: $D^2(D+2)=9\cdot 5=45$, the minimum rung for stable self-reference when spatial dimension is forced to $D=3$ (forcing chain T8). Status is a structural theorem with no sorry and no axioms.
The certificate structure demands three properties of a real-valued domain cost on mass/energy pairs and of a canonical threshold scalar. Domain cost is the local cost functional used in this gravity module; it is expected to sit at zero when the two arguments coincide (identity recognition) and to stay non-negative off the diagonal, mirroring the global J-cost non-negativity from ObserverForcing ("The cost of any recognition event is non-negative").
Sibling lemmas already establish diagonal vanishing, non-negativity for positive arguments, and positivity of the canonical threshold. This declaration only bundles them.
proof idea
One-line structure instance. The three fields of RSGRVStructural004Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning occurs here; noncomputable is inherited from the real-analytic cost infrastructure.
why it matters
Gives a single named inhabitant of the module-4 certificate type so downstream gravity developments can assume the gap-45 structural package in one hypothesis rather than three. The module frames this as the structural theorem for the minimum self-reference rung at $D=3$, tying directly to forcing-chain T8 (three spatial dimensions) and to the phi-ladder rung counting that places stable self-reference at gap 45. No used-by edges are recorded yet; the immediate consumer is the sibling cert_inhabited and any later GRV structural composition that requires the bundled certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.