cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single certificate for the RS dark-matter density module: diagonal vanishing, nonnegativity, and a positive canonical threshold. Cosmology authors assembling the structural Omega_DM claim cite this bundle rather than the three lemmas separately. The body is a pure structure instance that wires existing proofs.
Claim. There exists a certificate asserting that the 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
The module treats dark-matter density in Recognition Science units. Observationally $\Omega_{\mathrm{DM}}\approx 0.265$; RS writes $\Omega_{\mathrm{DM}}=\Omega_{\mathrm{tot}}-\Omega_b-\Omega_\Lambda=1-0.049-0.685=0.266$ and claims all three components arise from the same $J$-cost bookkeeping, so their sum recovers the total.
The certificate structure packages the minimal analytic properties of the local domain cost $C$: it vanishes on the diagonal away from zero, stays nonnegative on the positive quadrant, and sits below a strictly positive canonical threshold. Those three properties are the only hypotheses the density argument needs from the cost layer.
Upstream, nonnegativity of recognition cost is already known from the observer-forcing layer: every recognition event has $J$-cost at least zero because $J$ itself is nonnegative on the positive reals.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs.
why it matters
Gives the cosmology module a single named inhabitant of the dark-matter density certificate, so downstream density identities can assume the three cost axioms by projecting fields rather than re-proving them. The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and sits inside the broader RS program in which $\Omega_b$, $\Omega_\Lambda$, and $\Omega_{\mathrm{DM}}$ are all read off $J$-cost; the certificate is the local interface that makes that reading formal. No parent theorems currently depend on it in the graph, so it is a leaf packaging step rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.