cert
plain-language theorem explainer
Packages three structural facts about the cosmology domain cost into a single certificate: vanishing on the diagonal, non-negativity for positive arguments, and positivity of the canonical threshold. Cosmologists citing the RS dark-matter mass module (M_W/45) use this bundle as the certified interface. The definition is a pure structure inhabitant that wires three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS cosmology stack targets a dark-matter mass prediction $M_W/45=1.787,\mathrm{GeV}$, flagged as testable against the XENONnT program (2026). The local status line is structural theorem: zero sorry, zero axiom.
The certificate structure collects three properties of a two-argument domain cost on the reals. That cost is the module-level specialization of the Recognition J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Upstream, the foundation lemma cost_nonneg states that every recognition event has non-negative cost, via non-negativity of $J$ on positive states. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields of the certificate.
proof idea
One-line structure inhabitant. Each field of RSCosmo006Cert is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No additional tactics or algebraic work.
why it matters
This certificate is the certified export of Cosmology Module 6. Downstream consumers (none yet wired in the graph) would cite it rather than the three raw lemmas when invoking the DM-mass structural layer. In the broader RS chain it sits under the cost infrastructure forced by T5 (J-uniqueness) and the Recognition Composition Law; the module itself is marked TESTABLE via the XENONnT falsifier window. It does not compute the numerical mass; it only certifies the cost and threshold scaffolding that the mass claim rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.