RSGRVStructural007Cert
plain-language theorem explainer
Certificate bundle for RS gravity structural module 7: the domain recognition cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Gravity and cost-calculus authors cite it when discharging the J-ratio symmetry package. It is a pure structure definition; inhabitants are built by plugging in the three sibling lemmas.
Claim. A certificate consists of three facts: (i) for every $r \neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 7 of the RS gravity structural series records ratio symmetry of the recognition cost: $J(x)=J(1/x)$. In RS units the cost is the unique T5 functional $J(x)=(x+x^{-1})/2-1$, which is minimized at the identity $x=1$ with $J(1)=0$ and is nonnegative everywhere on $\mathbb{R}_{>0}$.
The domain cost here is the two-argument lift of that $J$ to a mass/energy (or scale/scale) pair; evaluating on the diagonal $m=e$ recovers the identity event. The canonical threshold is the positive cutoff used by the surrounding gravity certificates.
Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J$-cost nonnegativity. This module specializes that fact to the gravity domain cost and packages it with diagonal vanishing and threshold positivity.
proof idea
No proof body: the declaration is a structure (record type) with three propositional fields. Inhabitation is deferred to the sibling definition cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. Nonemptiness is then the one-line ⟨cert⟩.
why it matters
Gives the typed interface that module 7 exports as its structural theorem package (0 sorry, 0 axiom). Downstream, cert is the concrete inhabitant and cert_inhabited records Nonempty of the certificate type, so later gravity lemmas can assume the bundle rather than re-prove diagonal vanishing, nonnegativity, and threshold positivity.
In the broader RS chain this sits under T5 J-uniqueness and the Recognition Composition Law: ratio symmetry $J(x)=J(1/x)$ is exactly the statement that cost depends only on the dimensionless ratio, which gravity modules need when comparing mass and energy scales on the phi-ladder. It does not itself force $D=3$ or the eight-tick octave; those live in T7–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.