dmMassRatio_eq
plain-language theorem explainer
Recognition Science cosmologists cite the equality fixing the dark matter to W-boson mass ratio at one over forty-five. This pins the predicted dark matter mass near 1.79 GeV once the W mass is supplied. The proof is a one-line reflexivity step that follows directly from the definition of the ratio as the reciprocal of gap forty-five.
Claim. The dark matter mass ratio satisfies $m_{DM}/m_W = 1/45$.
background
The module develops the dark matter mass prediction from the gap-45 quantity in A6 cosmology. Gap-45 is defined as D squared times (D plus two) and equals forty-five at three spatial dimensions. The dark matter mass ratio is introduced as the rational number one divided by gap-45. Upstream the cosmology module sets the identical ratio directly to one over forty-five while the standard model supplies the W boson mass value of approximately 80.377 GeV. The module doc states the RS prediction m_DM equals m_W over gap-45.
proof idea
The proof is a one-line wrapper applying reflexivity to the definition of the dark matter mass ratio as one over gap-45 together with the prior equality gap-45 equals forty-five.
why it matters
This equality supplies the mass ratio input to the darkMatterMassCert definition that assembles the gap value, mass ratio and mass band. It completes the mass ratio step in the gap-45 dark matter prediction, consistent with the three-dimensional result from the forcing chain. The module reports zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.