sigma_DM_weak_ref_cm2
plain-language theorem explainer
sigma_DM_weak_ref_cm2 defines the absolute dark-matter cross section in cm² by scaling the neutrino weak reference with the RS ratio J(phi). Dark-matter phenomenologists normalizing signals to weak-interaction channels cite this when checking the derived band against detector thresholds. It is realized as a direct multiplication of the upstream ratio definition and the Fermi-derived reference value.
Claim. The reference dark-matter cross section is given by $J(phi) · sigma_nu_weak_ref_cm2$, where $J(phi) = phi - 3/2$ and $sigma_nu_weak_ref_cm2$ is the neutrino reference cross section in cm² obtained from the Fermi constant scorecard at 1 GeV.
background
The module implements the P0-A6 weak neutrino-reference cross-section scorecard. It sets the reference energy to 1 GeV and converts the Fermi prediction to cm², producing the interval 5.2e-38 < sigma_nu_weak_ref_cm2 < 5.4e-38. The upstream ratio sigma_DM_over_sigma_nu_RS is defined as phi - 3/2, identified with J(phi) from the Recognition Composition Law. This definition multiplies the ratio by the reference to obtain the absolute dark-matter cross section on the same channel.
proof idea
One-line wrapper that multiplies sigma_DM_over_sigma_nu_RS by sigma_nu_weak_ref_cm2.
why it matters
It supplies the numerical value asserted inside the DarkMatterWeakReferenceCrossSectionScoreCardCert structure for the sigma_dm_band interval 5.7e-39 < sigma_DM_weak_ref_cm2 < 7.1e-39. The theorem row_sigma_DM_weak_ref_band then proves those bounds by unfolding this definition together with the ratio and reference bands. Within the Recognition framework this closes the arithmetic step of P0-A6, linking the J(phi) ratio from forcing-chain step T5 to observable cross-section limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.