cert
plain-language theorem explainer
Packages three proved facts about the gravity-domain recognition cost into one certificate: the cost vanishes when the two arguments agree, stays non-negative for positive mass and energy, and the canonical threshold is strictly positive. Gravity and RS structural audits cite it as the inhabited witness for module 7 (J-cost ratio symmetry). The body is a pure structure assembly of three sibling lemmas.
Claim. There is an inhabited certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 7 records the structural fact that Recognition Science cost is ratio-symmetric: the J-cost satisfies $J(x)=J(1/x)$. In RS units the cost functional is the unique continuous solution of the Recognition Composition Law forced at T5, namely $J(x)=(x+x^{-1})/2-1$, which is minimized at the identity $x=1$ and is invariant under inversion.
Here the domain cost is the gravity-facing specialization of that J-cost on a pair of positive scale parameters (mass-like and energy-like). The certificate structure bundles three elementary properties of that specialization: diagonal vanishing, nonnegativity, and positivity of a fixed canonical threshold used as a comparison scale.
Upstream, nonnegativity of recognition cost is already known in the observer-forcing layer: every recognition event has cost at least zero because $J$ itself is nonnegative on the positive reals.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on the positive quadrant), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site.
why it matters
Gives a single named witness that the gravity-domain cost obeys the three structural axioms expected from J-cost ratio symmetry. That symmetry is the content of this structural module (0 sorry, 0 axiom) and sits downstream of T5 J-uniqueness in the forcing chain. With no further used-by edges yet, the certificate is the export surface for later GRV or phenomenology lemmas that need a packaged nonnegativity-plus-threshold hypothesis rather than three separate facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.