cert
plain-language theorem explainer
Packages three proved structural facts (domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive) into one inhabited certificate for Gravity structural module 6. Anyone citing the module's phi-uniqueness / self-similar-fixed-point package would point here. The body is a pure field assembly: three sibling lemmas are plugged into the certificate structure.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{domainCost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{domainCost}(m,e)\ge 0$; and (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS gravity structural series records the uniqueness of $\varphi$ as the self-similar fixed point $\varphi=1+1/(1+1/(1+\cdots))$, status structural (zero sorry, zero axiom). The certificate type bundles three elementary cost/threshold properties that the module treats as the local structural interface.
Domain cost is the module's real-valued cost on pairs of positive scales; the diagonal vanishing clause says equal arguments incur zero cost, matching the J-cost minimum at identity. Nonnegativity for positive mass/energy arguments is the local form of the global fact that recognition cost is nonnegative (upstream: any recognition event has $0\le e.\mathrm{cost}$, via $J$-cost nonnegativity). The canonical threshold is the module's positive cutoff scale against which those costs are compared.
The certificate is the single object that packages those three Prop fields so downstream gravity lemmas can assume one inhabited record rather than three separate hypotheses.
proof idea
One-line structure inhabitant. The three fields of RSGRVStructural006Cert are filled by the sibling lemmas already proved in-module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the cutoff by canonicalThreshold_pos. No further tactic work; the def is pure field wiring.
why it matters
Gives the inhabited structural certificate for Gravity module 6, whose stated content is RS $\varphi$ uniqueness as the self-similar fixed point (primer landmark T6). Downstream consumers of the module can take one certificate rather than re-proving diagonal vanishing, cost nonnegativity, and threshold positivity. The nonnegativity field is the local echo of the foundation result that every recognition event has nonnegative cost. No used_by edges are recorded yet; the sibling cert_inhabited is the natural next consumer. Closes the structural interface of this module with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.