pith. sign in
module module moderate

IndisputableMonolith.Physics.DarkMatterMassFromGap45

show as:
view Lean formalization →

The module assembles definitions that set the dark matter to W-boson mass ratio equal to the reciprocal of gap45 on the phi-ladder. Particle physicists examining mass hierarchies or dark matter candidates would cite the resulting mDM_GeV and certification object. The module consists of named constants, equalities, and a certification wrapper with no internal proofs.

claim$ m_{\mathrm{DM}} / m_W = 1 / \mathrm{gap45} $

background

Recognition Science places particle masses on a phi-ladder whose rungs follow yardstick * phi^(rung - 8 + gap(Z)). gap45 supplies the gap term at rung 45 that isolates the dark matter sector relative to the W boson. The module works inside the forcing chain (T0-T8) and the Recognition Composition Law, importing only Mathlib for numeric support.

The sibling definitions introduce gap45 and gap45_eq, then dmMassRatio together with its equality, followed by concrete GeV values mW_GeV and mDM_GeV and the band mDM_band. DarkMatterMassCert packages these into a single certified object.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the explicit ratio that enters DarkMatterMassCert and thereby links the phi-ladder mass formula to a concrete dark matter prediction. It fills the gap parameter slot required by the T5-T8 chain and the mass formula yardstick * phi^(rung - 8 + gap(Z)). No downstream theorems are recorded, so the module serves as a leaf that other certification objects can reference.

scope and limits

declarations in this module (9)