pith. sign in
module module moderate

IndisputableMonolith.Cosmology.DarkMatterXENONPrediction

show as:
view Lean formalization →

The module predicts that dark matter mass over W boson mass equals 1/45 in RS units, together with the associated cross-section ratio for XENON detection. Cosmologists and direct-detection experimentalists would cite it when mapping the phi-ladder mass formula onto observable signals. The module assembles the claim through ratio definitions, positivity lemmas, band membership checks, and a final certification theorem.

claim$m_{DM}/m_W = 1/45$, with the corresponding cross-section ratio lying inside the XENON experimental band.

background

The module imports the fundamental RS time quantum τ₀ = 1 tick from Constants and the cost functions from the Cost module. These supply the J-cost and defect-distance machinery used to assign masses on the phi-ladder. The local theoretical setting is the cosmology domain, where the mass formula yardstick · ϕ^(rung − 8 + gap(Z)) is specialized to the dark-matter candidate, producing the stated ratio to the W boson.

proof idea

This is a definition module. It introduces dmMassRatio and dmCrossSectionRatio as the concrete numerical predictions, then proves dmCrossSection_pos and dmCrossSection_in_band before packaging the results in the DarkMatterXENONCert theorem.

why it matters in Recognition Science

The module supplies the terminal numerical prediction that realizes the phi-ladder mass assignment for dark matter and feeds it directly into XENON bounds. It closes the loop from the unified forcing chain (T5–T8) to an observable cross-section ratio, with the certification theorem serving as the interface to experimental cosmology.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)