row_sigma_DM_weak_ref_band
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 in Recognition Science
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.
scope and limits
- Does not derive the value of the Fermi constant.
- Does not prove the ratio equals J(phi) from first principles.
- Does not address other reference energies.
- Does not claim experimental confirmation.
- Does not cover strong-interaction channels.
formal statement (Lean)
63theorem row_sigma_DM_weak_ref_band :
64 5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39 := by
proof body
Tactic-mode proof.
65 unfold sigma_DM_weak_ref_cm2
66 have href := row_weak_ref_cross_section_band
67 have hratio := row_sigma_ratio_band
68 have href_pos : 0 < sigma_nu_weak_ref_cm2 := by linarith [href.1]
69 have hratio_pos : 0 < sigma_DM_over_sigma_nu_RS := by linarith [hratio.1]
70 constructor
71 · nlinarith [href.1, hratio.1, href_pos, hratio_pos]
72 · nlinarith [href.2, hratio.2, href_pos, hratio_pos]
73