cert
plain-language theorem explainer
Packages three structural facts about the gravity-domain cost into a single certificate: the cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Gravity and RS-forcing auditors cite it as the inhabited witness that Module 9's cost setup is well-formed. The body is a pure structure instance wiring three already-proved sibling lemmas.
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 $T$ obeys $T>0$.
background
Module 9 sits in the Gravity lane of the RS forcing chain (T5 J-uniqueness through T8, $D=3$). It treats a real-valued domain cost $C(m,e)$ on mass/energy-like arguments, together with a fixed positive canonical threshold used as a structural cutoff.
The certificate structure demands three properties: diagonal vanishing ($C(r,r)=0$ off zero), non-negativity on the positive quadrant, and positivity of the threshold. Non-negativity is the gravity-domain shadow of the global fact that recognition cost is non-negative: upstream, any recognition event has cost $\ge 0$ because the J-cost $J$ is non-negative on positive reals.
Local siblings supply the three field proofs (domainCost on the diagonal, its non-negativity lemma, and positivity of canonicalThreshold). This definition only assembles them.
proof idea
Definitional structure instance, not a tactic proof. The three fields of the certificate are filled by direct assignment to the sibling lemmas: diagonal identity from the domain-cost-at-equality result, non-negativity from the domain-cost non-negativity lemma, and threshold positivity from the canonical-threshold positivity lemma. No further rewriting or case analysis occurs.
why it matters
Gives Module 9 a single named witness that its cost/threshold package is coherent, matching the module claim of a structural theorem with zero sorry and zero axiom. In the RS gravity stack this is the bookkeeping step that lets later structural results assume diagonal vanishing, cost positivity, and a positive cutoff without re-proving them.
It sits under the forcing landmarks T5 (J-uniqueness / J-cost) through T8 ($D=3$): the non-negativity field is the local echo of J-cost non-negativity from observer forcing. No downstream consumers are recorded yet; the natural next use is the inhabitedness lemma for the same certificate type, and any gravity structural theorem that needs a bundled well-formedness hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.