Prove2Me

Lower limit 1–2 GeV on detectable halo-particle masses (aluminium target)

Proved
GoodmanWitten.lower_mass_limit_aluminium

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

dark-mattermathematical-physicsparticle-physics

Let the halo velocity be v=200v = 200 km/s, i.e. β=v/c=2×107/(2.99792458×1010)\beta = v/c = 2\times10^{7}/(2.99792458\times10^{10}), and let the target be aluminium, A=27A=27, with nuclear mass M=27 mNM = 27\,m_N. Let the detector threshold ϵ\epsilon (in GeV) satisfy

50 eV≤ϵ≤100 eV.50\ \mathrm{eV} \le \epsilon \le 100\ \mathrm{eV}.

Then there is a mass mmin⁡m_{\min} with 1 GeV≤mmin⁡≤2 GeV1\ \mathrm{GeV} \le m_{\min} \le 2\ \mathrm{GeV} such that, for every m>0m>0,

(2mβ)22M≥ϵ  ⟺  m≥mmin⁡.\frac{(2m\beta)^2}{2M} \ge \epsilon \iff m \ge m_{\min}.

That is, a halo particle can deposit the threshold energy only if its mass is at least mmin⁡∈[1,2]m_{\min}\in[1,2] GeV.

This is the paper's lower limit on the mass of detectable halo particles.

Formalization Note Energies are in GeV, so 5050 eV is written 50e-9.

Preamble
import Mathlib
import Definitions.Def_GoodmanWitten_basic
Formal statement
namespace GoodmanWitten

theorem lower_mass_limit_aluminium (ε : ℝ) (hε₁ : 50e-9 ≤ ε) (hε₂ : ε ≤ 100e-9) :
    ∃ mmin : ℝ, 1 ≤ mmin ∧ mmin ≤ 2 ∧
      ∀ m : ℝ, 0 < m →
        (ε ≤ maxRecoilEnergy m (nucleusMass 27) (2e7 / speedOfLight) ↔ mmin ≤ m) := by sorry

end GoodmanWitten
Source
M. W. Goodman and E. Witten, Detectability of certain dark-matter candidates, Phys. Rev. D 31, 3059-3063 (1985), https://doi.org/10.1103/PhysRevD.31.3059, p. 3059, right column, paragraph 2
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph