RSGRVStructural004Cert
plain-language theorem explainer
Certificate bundle for Gravity structural module 4 (RS gap-45): diagonal domain cost vanishes, domain cost is nonnegative on positive masses and energies, and the canonical threshold is strictly positive. Gravity and ladder auditors cite it as the typed interface that module 4 must inhabit. The structure itself is pure data; inhabitance is discharged by the sibling lemmas on domainCost and the threshold.
Claim. A certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_GRV_Structural_004 packages the gap-45 structural claim of Recognition Science gravity: at spatial dimension $D=3$, the combination $D^2(D+2)=9\cdot 5=45$ is the minimum rung for stable self-reference. Status is structural (no sorry, no axioms).
The domain cost is the local cost functional on pairs of positive reals used in this gravity layer; its diagonal vanishing and nonnegativity mirror the global J-cost story. Upstream, ObserverForcing records that every recognition event has nonnegative cost via Cost.Jcost_nonneg on a positive state. The canonical threshold is the positive cutoff against which domain-cost comparisons are made in the module.
This declaration does not prove those facts. It only names the Prop triple that a concrete certificate must supply.
proof idea
No proof body: this is a structure definition. The three fields are pure propositions (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is separate: the sibling cert fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited wraps that as Nonempty.
why it matters
In the gravity structural stack this is the typed gate for module 4. Downstream, cert builds a concrete inhabitant and cert_inhabited asserts nonemptiness, so any later gravity lemma that needs gap-45 bookkeeping can depend on a single certificate rather than three loose lemmas.
Framework-wise it sits under the D=3 forcing (T8) and the eight-tick / rung ladder: gap-45 is advertised as the minimum rung for stable self-reference at three spatial dimensions. The cost fields keep the gravity layer aligned with the global nonnegative J-cost discipline from ObserverForcing and the Cost module. It closes no open physics conjecture by itself; it freezes the interface that the structural theorem claims to satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.