Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.DarkMatterXENONPrediction

show as:
view Lean formalization →

The module predicts the dark matter mass to W boson mass ratio equals 1/45 within Recognition Science cosmology. Particle physicists and cosmologists testing XENON bounds would cite the result for model constraints. It consists of sibling definitions for the mass ratio, cross-section ratio, positivity, band membership, and a certification object.

claimThe predicted ratio satisfies $m_{ m DM}/m_W=1/45$.

background

The module sits in the cosmology domain and imports the RS time quantum $ au_0=1$ tick from Constants together with cost structures from Cost. It defines dmMassRatio, dmCrossSectionRatio, dmCrossSection_pos, dmCrossSection_in_band, DarkMatterXENONCert and darkMatterXENONCert as the concrete objects realizing the prediction. These rest on the J-cost and phi-ladder conventions already fixed in the imported modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the explicit DM mass prediction stated in its doc-comment, which would feed any downstream certification of XENON-compatible dark matter within the Recognition framework. It realizes the mass-ratio step that connects the phi-ladder mass formula to observable cosmology.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)