cert
plain-language theorem explainer
Packages three structural facts about the astrophysics domain cost into a single certificate: it vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the RS structural astrophysics layer (module 10) uses this bundle. The definition simply wires three already-proved field lemmas into the certificate structure.
Claim. There is a structural 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 10 is the RS structural astrophysics layer. Calibration is fixed once by the electron mass via the coherence energy $E_{\mathrm{coh}}$; thereafter predictions are parameter-free. The status line records a structural theorem with no sorry and no extra axioms.
The domain cost is the local cost functional comparing a model value to an evidence value. It is built from the Recognition Science $J$-cost (the unique symmetric cost forced by the Recognition Composition Law), so nonnegativity and diagonal vanishing are the expected algebraic properties. The canonical threshold is the positive cutoff used to separate structural agreement from disagreement in this module.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: any recognition event has nonnegative cost because $J$ is nonnegative on the positive reals. The three field lemmas assembled here specialize that picture to the astrophysics domain cost and threshold.
proof idea
One-line structure instance. The three certificate fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further calculation occurs in the definition body.
why it matters
This certificate is the packaged witness that module 10's cost geometry is well-formed: zero self-cost, nonnegative mismatch cost, and a usable positive threshold. Downstream consumers of the structural astrophysics layer can take the whole bundle rather than re-prove the three facts. In the broader RS stack it supports the claim that, once $E_{\mathrm{coh}}$ is fixed by the electron mass, astrophysical structural comparisons run parameter-free on the forced $J$-cost. It does not itself derive masses, rotation curves, or the alpha band; it only certifies the cost/threshold scaffolding those predictions sit on. No used-by edges are recorded yet, so its immediate role is as the inhabited certificate for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.