RSCosmo006Cert
plain-language theorem explainer
Certificate bundle for Cosmology Module 6: the domain cost vanishes on equal positive arguments, stays non-negative for positive mass and energy scales, and the canonical detection threshold is strictly positive. Cosmology and DM-search readers cite it as the structural interface behind the M_W/45 mass claim and the XENONnT falsifier. It is a pure structure; inhabitance is discharged by wiring three local lemmas.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (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}$ and flags a concrete 2026 XENONnT falsifier. Status is structural: zero sorry, zero axioms.
The domain cost is the local cost functional on mass/energy scale pairs used by this module; the certificate demands it behave like a true cost (zero on the diagonal, nonnegative off it). The canonical threshold is the positive cutoff against which a detection or exclusion claim is judged.
Upstream, recognition costs are already known to be nonnegative: ObserverForcing records that every recognition event has cost $0 \le e.\mathrm{cost}$, via nonnegativity of the $J$-cost. The present structure lifts that discipline into the cosmology domain-cost interface.
proof idea
No proof body: this is a structure declaration packing three propositions as fields. Inhabitation is separate. The sibling definition cert fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then exhibits Nonempty via that witness. The only external cost fact in the dependency cone is the foundation nonnegativity of recognition-event cost.
why it matters
Gives Module 6 a single named certificate type so downstream code can require the cost and threshold package without restating three separate lemmas. Parents in-module are the concrete witness cert and the inhabitance theorem cert_inhabited, which close the structural claim for the DM-mass / XENONnT story.
In the broader RS picture this is bookkeeping on the cost side of a testable cosmology prediction, not a forcing-chain step (T5–T8). It keeps the module’s “STRUCTURAL THEOREM” status honest: the physics claim is pinned to a positive threshold and a well-behaved domain cost rather than to an open axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.