darkMatterMassCert
plain-language theorem explainer
The declaration constructs a certificate packaging the Recognition Science dark matter mass prediction m_DM = m_W / 45 together with the numerical band 1.77 to 1.80 GeV. Cosmologists working in A6 cosmology would cite it when referencing the gap-45 derived ratio at D=3. The definition is a direct record construction that populates the three fields from sibling equalities.
Claim. The certificate asserts gap_{45} = 45, dmMassRatio = 1/45, and 1.77 < m_{DM,GeV} < 1.80.
background
The module states the RS prediction m_DM = m_W / gap-45 with m_W ≈ 80.4 GeV yielding m_DM ≈ 1.787 GeV and band (1.77, 1.79) GeV. Gap-45 is defined as D²(D+2) = 45 at D=3. The structure DarkMatterMassCert packages three assertions: gap45_val : gap45 = 45, mass_ratio : dmMassRatio = 1/45, and mDM_band : 1.77 < mDM_GeV < 1.80.
proof idea
The definition constructs the DarkMatterMassCert record by direct field assignment: gap45_val receives the equality from gap45_eq, mass_ratio receives the equality from dmMassRatio_eq, and mDM_band receives the interval from mDM_band. No tactics or reductions occur beyond record construction.
why it matters
This definition supplies the packaged certificate for the dark matter mass prediction in the RS A6 cosmology section, relying on the D=3 gap formula from the forcing chain (T8). It draws on upstream gap45_eq results from CardinalitySpectrum and RSCoupledAxis. No downstream uses appear yet, leaving open its integration into broader mass-ladder calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.