Prove2Me

Coherent weak rates of order 10410^4 events/kg day for m∼Mm\sim M

Proved
GoodmanWitten.coherent_rate_order_1e4

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

dark-mattermathematical-physicsparticle-physics

Let the target have mass number A>0A>0 and nuclear mass M=A mNM = A\,m_N, and consider a halo particle with coherent weak interactions of mass m=Mm = M, with Yˉ=1\bar Y = 1 and Nˉ=100\bar N = 100, halo density ρ=10−24\rho = 10^{-24} g/cm3^3 and velocity v=200v = 200 km/s. Then the counting rate R=KFσR = KF\sigma with the coherent cross section satisfies

104≤R<105events/kg/day,10^4 \le R < 10^5 \quad\text{events/kg/day},

i.e. the rate is of order 10410^4 events per kilogram per day.

Formalization Note "Of order 10410^4" is read as 104≤R<10510^4 \le R < 10^5; "m∼Mm\sim M, Yˉ∼1\bar Y\sim1, Nˉ∼100\bar N\sim100" is read as the exact values m=Mm=M, Yˉ=1\bar Y=1, Nˉ=100\bar N=100.

Preamble
import Mathlib
import Definitions.Def_GoodmanWitten_basic
Formal statement
namespace GoodmanWitten

theorem coherent_rate_order_1e4 (A : ℝ) (hA : 0 < A) :
    1e4 ≤ eventRatePerKgDay A (coherentCrossSection (nucleusMass A) (nucleusMass A) 1 100)
        1e-24 2e7 (nucleusMass A) ∧
      eventRatePerKgDay A (coherentCrossSection (nucleusMass A) (nucleusMass A) 1 100)
        1e-24 2e7 (nucleusMass A) < 1e5 := 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. 3060, left column, paragraph after Eq. (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