cert
plain-language theorem explainer
Packages three gravity-domain cost facts into one RS structural certificate: diagonal vanishing, nonnegativity for positive mass and energy scale, and a strictly positive canonical threshold. Gravity and recognition-cost workers cite it when they need the bundled hypotheses rather than the separate lemmas. The definition is a structure instance that wires three already-proved sibling fields.
Claim. There is a certificate recording that the gravity domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $\tau$ obeys $\tau>0$.
background
This module is Gravity RS Structural Module 3. Its stated content is the RS count law $2^D-1=7$ independent channels, exact once spatial dimension is fixed at $D=3$ (the T8 landmark of the forcing chain). Status is structural: zero sorry, zero axiom.
The certificate type collects three properties of a domain cost $C$ on positive real mass and energy-scale arguments: vanishing on the diagonal $C(r,r)=0$ for $r\neq 0$; nonnegativity $C(m,e)\ge 0$ for $m,e>0$; and positivity of a fixed canonical threshold. Nonnegativity is the gravity-domain shadow of the general fact that every recognition event has nonnegative cost, which follows from nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ on positive reals.
Sibling lemmas supply each field: diagonal identity, domain nonnegativity, and threshold positivity. The present declaration only assembles them.
proof idea
Pure structure construction, not a tactic proof. The three fields of the certificate are filled by direct assignment: diagonal vanishing from the sibling domainCost_at_eq, nonnegativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No further rewriting or case analysis occurs at this site.
why it matters
Gives a single named inhabitant of the structural certificate used by the gravity RS count-law layer (seven independent channels from $D=3$). Downstream use list is currently empty, so the value is organizational: later gravity lemmas can depend on one certificate rather than three scattered facts.
It sits under the structural theorem banner of the module (RS count law exact from configuration dimension three) and inherits the J-cost nonnegativity lineage from observer forcing. It does not itself derive $2^D-1=7$ or close any open physics claim; it only packages cost hygiene needed for that structural story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.