sigma_DM_cm2
plain-language theorem explainer
The definition computes the absolute dark-matter cross section in cm² by multiplying the RS-native ratio sigma_DM_over_sigma_nu_RS by the protocol reference sigma_nu_reference_cm2. Dark-matter detection groups would cite it when mapping predicted bands to experimental limits. It is realized by direct multiplication of the two upstream definitions.
Claim. The absolute dark-matter cross section is given by $σ_{DM} = (σ_{DM}/σ_ν)_{RS} × σ_{ν,ref}$ where $(σ_{DM}/σ_ν)_{RS} = ϕ - 3/2$ and $σ_{ν,ref} = 10^{-38}$ cm².
background
This definition belongs to the P0-A6 scorecard module for absolute cross-section normalization. The module states the formula sigma_DM = (sigma_DM/sigma_nu) * sigma_nu_ref with the band 0.11 < ratio < 0.13 and reference value 1e-38 cm²; the derived absolute band is (1.1e-39, 1.3e-39) cm² once a sub-0.35 keV efficiency curve is supplied. The local setting treats the reference as a protocol choice whose RS derivation remains open.
proof idea
One-line definition that multiplies the upstream ratio definition by the upstream reference definition.
why it matters
The definition supplies the concrete value required by the DarkMatterAbsoluteCrossSectionScoreCardCert structure and by the row_sigma_DM_cm2_band theorem that certifies the absolute band. It completes the P0-A6 row by converting the native J(phi) ratio into an absolute prediction in cm². The open question noted in the module is deriving the reference normalization from RS axioms or a specified neutrino channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.