Hard-sphere cross section $\sigma\approx2.0A^{2/3}\times10^{-25}$ cm $^2$

Proved

GoodmanWitten.strong_cross_section_estimate

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

dark-mattermathematical-physicsparticle-physics

Let a strongly interacting particle scatter from a nucleus of mass number $A>0$ through a square-well potential of radius $R = 1.25A^{1/3}\times10^{-13}$ cm, with low-energy cross section $\sigma = 4\pi R^2$ . Then there is a constant $C$ with $|C/2.0 - 1|\le0.05$ such that for all $A>0$

\sigma = C\,A^{2/3}\times10^{-25}\ \mathrm{cm}^2 .

Formalization Note 5% relative tolerance on the printed coefficient.

Preamble

import Mathlib
import Definitions.Def_GoodmanWitten_basic

Formal statement

namespace GoodmanWitten

theorem strong_cross_section_estimate : ∃ C : ℝ, |C / 2.0 - 1| ≤ 0.05 ∧
    ∀ A : ℝ, 0 < A → strongCrossSection A = C * A ^ ((2 : ℝ) / 3) * 1e-25 := 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. 3062, right column, section (iii), 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

Hard-sphere cross section σ≈2.0A2/3×10−25\sigma\approx2.0A^{2/3}\times10^{-25}σ≈2.0A2/3×10−25 cm2^22

Hard-sphere cross section $\sigma\approx2.0A^{2/3}\times10^{-25}$ cm $^2$