row_sigma_DM_cm2_band
plain-language theorem explainer
row_sigma_DM_cm2_band establishes the absolute dark-matter cross-section band in cm² as lying between 1.1e-39 and 1.3e-39. Dark-matter experimentalists would cite this when setting sensitivity targets against the Recognition Science prediction. The proof unfolds the product definition of sigma_DM_cm2 and transfers the ratio bounds via linear arithmetic.
Claim. The predicted absolute dark matter cross section satisfies $1.1 × 10^{-39} < σ_{DM} < 1.3 × 10^{-39}$ in cm², obtained by scaling the ratio band $0.11 < σ_{DM}/σ_ν < 0.13$ by the reference value $10^{-38}$ cm².
background
sigma_DM_cm2 is defined as the product of the RS-derived ratio sigma_DM_over_sigma_nu_RS and the fixed protocol reference sigma_nu_reference_cm2 equal to 10^{-38} cm². The ratio bounds 0.11 to 0.13 are supplied by the upstream theorem row_sigma_ratio_band, which rests on the golden-ratio inequalities phi_gt_onePointSixOne and phi_lt_onePointSixTwo. This theorem belongs to the P0-A6 scorecard module, whose documentation specifies that the band applies to detector comparisons only after supplying a sub-0.35 keV efficiency curve, and notes that deriving the reference normalization from the Recognition Science equation remains open.
proof idea
The proof unfolds sigma_DM_cm2 and sigma_nu_reference_cm2 to reveal the multiplication by the ratio. It obtains the ratio bounds from row_sigma_ratio_band and applies nlinarith to each side of the conjunction to scale the inequalities by the reference value.
why it matters
This supplies the absolute band component for the certificate darkMatterAbsoluteCrossSectionScoreCardCert_holds, which assembles the three rows into a single Nonempty cert object. It fills the numerical target in the P0-A6 absolute cross-section normalization scorecard. The module documentation identifies the open task of grounding the reference value in the RS functional equation or a concrete neutrino channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.