row_sigma_DM_weak_ref_band
plain-language theorem explainer
The theorem pins the dark-matter weak-reference cross section to the interval (5.7e-39, 7.1e-39) cm². Dark-matter experimentalists normalizing against neutrino scattering would cite this bound when comparing to J(phi)-driven predictions. The proof multiplies the established neutrino reference band by the J(phi) ratio band and propagates the inequalities with nlinarith after confirming positivity.
Claim. $5.7times10^{-39} < sigma_{DM,weak} < 7.1times10^{-39}$ cm², where $sigma_{DM,weak} := (phi - 3/2) cdot sigma_{nu,weak}$ and $sigma_{nu,weak}$ lies in $(5.2times10^{-38}, 5.4times10^{-38})$ cm² from the Fermi constant at 1 GeV.
background
In the P0-A6 scorecard the weak neutrino reference channel supplies the normalization for dark-matter cross sections. The ratio sigma_DM_over_sigma_nu_RS is defined as phi - 3/2, which equals J(phi) in the Recognition framework. The neutrino reference cross section sigma_nu_weak_ref_cm2 is obtained by squaring the Fermi prediction, multiplying by E_ref_GeV squared, and converting units with gev2_to_cm2. The upstream theorem row_weak_ref_cross_section_band supplies the interval 5.2e-38 < sigma_nu_weak_ref_cm2 < 5.4e-38, while row_sigma_ratio_band supplies 0.11 < phi - 3/2 < 0.13.
proof idea
The proof unfolds sigma_DM_weak_ref_cm2 to the product of the ratio and the neutrino reference. It imports the two band theorems, establishes positivity of both factors by linarith, then applies nlinarith to each side of the target inequality using the four bounds.
why it matters
This result populates the sigma_dm_band field inside the certificate darkMatterWeakReferenceCrossSectionScoreCardCert_holds. It closes the arithmetic step of P0-A6 by propagating the J(phi) ratio through the weak reference channel. The module doc notes that the 1 GeV choice remains a protocol normalization whose falsifier is a sub-0.35 keV detector excluding the derived band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.