cert
plain-language theorem explainer
Packages three elementary properties of the gravity domain cost into one certificate: vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Gravity and calibration proofs that need a single inhabited structural witness cite this object. The definition is a pure field assembly of three sibling lemmas already proved in the module.
Claim. There is a structural certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 10 of the RS gravity structural layer fixes the coherence energy $E_{\mathrm{coh}}$ once from the electron mass and then treats all further gravity predictions as parameter-free. The local cost on mass/energy pairs is the domain cost, a real-valued function built from the Recognition Science $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
The certificate structure bundles three elementary facts about that cost and a fixed positive threshold used as a comparison scale. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on the positive reals. The present module specializes that idea to the gravity domain cost and adds the diagonal-vanishing and threshold-positivity clauses.
proof idea
One-line structure instance. Each field is filled by a named sibling lemma already in the module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra tactics or algebraic work occur at this declaration.
why it matters
Gives a single inhabited witness that the gravity domain cost meets the structural checklist required by the RS gravity layer (zero on equal arguments, nonnegative off-diagonal, positive threshold). The module is marked structural with zero sorry and zero axioms, and calibrates $E_{\mathrm{coh}}$ once from the electron mass so later gravity predictions stay parameter-free. No downstream consumers are recorded yet; the natural parent is any theorem that assumes an RSGRVStructural010Cert rather than re-proving the three clauses. Ties to the broader forcing chain only indirectly via the $J$-cost nonnegativity inherited from ObserverForcing (T5 uniqueness of $J$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.