RSGRVStructural010Cert
plain-language theorem explainer
A certificate packing three structural facts for RS gravity module 10: the domain cost vanishes on equal arguments, stays non-negative for positive mass and energy, and the canonical threshold is strictly positive. Gravity and calibration proofs cite it as the single inhabited bundle of those axioms. It is a pure structure definition; inhabitance is discharged elsewhere by the concrete lemmas on domain cost and the threshold.
Claim. A certificate consists of three properties: (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 records the calibration stance: the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free. The local objects are a domain cost (a real-valued cost on a pair of positive scale parameters, typically mass-like and energy-like) and a canonical threshold used as a positivity cut.
Upstream, recognition cost is already known to be nonnegative: any recognition event has cost $0 \le e.\mathrm{cost}$, via nonnegativity of the $J$-cost on positive states. The certificate rephrases that discipline at the gravity-domain level: cost vanishes on the diagonal (balanced arguments) and never goes negative off it, while the threshold that gates the structural claims stays positive.
The structure itself carries no proof; it only names the three propositions that a later inhabitant must supply.
proof idea
No proof body: this is a structure declaration. The three fields are proposition-typed requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is separate: the definition cert fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited packages that as Nonempty.
why it matters
The certificate is the typed interface for structural gravity module 10. Downstream, cert builds a concrete inhabitant and cert_inhabited asserts the type is nonempty, so later gravity lemmas can assume the bundle rather than re-prove diagonal vanishing, cost nonnegativity, and threshold positivity each time.
In the broader RS stack this sits under the gravity domain after the forcing chain has fixed $J$, $\varphi$, the eight-tick octave, and $D=3$. Nonnegativity echoes the foundation fact that recognition cost never goes below zero. The module claim is structural and parameter-free once $E_{\mathrm{coh}}$ is set by the electron mass; the certificate is the Lean packaging of that structural stance, not a new dynamical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.