Encyclopedia Physics Physics Dark Matter Weak Reference Cross Section Score Card
ARTICLE 3 claims 3 theorems
Physics Dark Matter Weak Reference Cross Section Score Card
A machine-checked scorecard that turns a neutrino cross-section measurement into a narrow predicted band for dark matter interactions.
The weak reference scorecard
The weak reference cross section scorecard is a formal object in the Recognition Science library: a machine-checked collection of theorems that connects a standard neutrino interaction rate to a predicted range for dark matter scattering. The scorecard's purpose is to give experimentalists a concrete, falsifiable target. It computes a reference value for a neutrino interacting at 1 GeV, then scales that value by a ratio derived from the framework's cost function to produce a dark matter cross-section band.
The starting point is the Fermi constant, a measured quantity that sets the strength of the weak nuclear force. The reference cross-section formula is σν = GF² × Eref², with Eref = 1 GeV and a conversion factor of 0.3894 × 10⁻²⁷ cm²/GeV⁻². The scorecard proves, with no unproven axioms, that this reference value falls between 5.2 × 10⁻³⁸ and 5.4 × 10⁻³⁸ cm². This is the neutrino channel that a detector would use to normalize its own sensitivity.
The dark matter prediction follows from a ratio. The framework's cost function, which models the unavoidable expense of any recognition event, forces a specific ratio between dark matter and neutrino cross-sections: between 0.11 and 0.13. Multiplying the neutrino reference band by this ratio gives the dark matter band, proved to lie between 5.7 × 10⁻³⁹ and 7.1 × 10⁻³⁹ cm². This is the number a dark matter experiment can check.
The scorecard is honest about its limits. The arithmetic from the Fermi constant to the neutrino band is a theorem. The choice of a 1 GeV neutrino as the reference channel is a protocol normalization, a definitional choice, not a derived result. The falsifier is explicit: if a detector with sub-0.35 keV energy resolution excludes the derived band, the framework's prediction is wrong. The scorecard does not claim to explain dark matter's composition, only to predict where its scattering signal should appear.
THEOREM row_weak_ref_cross_section_band · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
theorem row_weak_ref_cross_section_band :
5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38 := by
unfold sigma_nu_weak_ref_cm2 E_ref_GeV gev2_to_cm2
have hgf := row_fermi_pred_bracket
have hgf_pos : 0 < row_fermi_pred := by linarith [hgf.1]
constructor
· nlinarith [hgf.1, hgf_pos]
· nlinarith [hgf.2, hgf_pos]
THEOREM row_sigma_DM_weak_ref_band · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
theorem row_sigma_DM_weak_ref_band :
5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39 := by
unfold sigma_DM_weak_ref_cm2
have href := row_weak_ref_cross_section_band
have hratio := row_sigma_ratio_band
have href_pos : 0 < sigma_nu_weak_ref_cm2 := by linarith [href.1]
have hratio_pos : 0 < sigma_DM_over_sigma_nu_RS := by linarith [hratio.1]
constructor
· nlinarith [href.1, hratio.1, href_pos, hratio_pos]
· nlinarith [href.2, hratio.2, href_pos, hratio_pos]
THEOREM darkMatterWeakReferenceCrossSectionScoreCardCert_holds · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
theorem darkMatterWeakReferenceCrossSectionScoreCardCert_holds :
Nonempty DarkMatterWeakReferenceCrossSectionScoreCardCert :=
⟨{ weak_ref_band := row_weak_ref_cross_section_band
sigma_dm_band := row_sigma_DM_weak_ref_band
fermi_bracket := row_fermi_pred_bracket
sigma_ratio_band := row_sigma_ratio_band }⟩
What this page does not claim
The scorecard does not identify what dark matter is made of. The choice of a 1 GeV neutrino reference energy is a protocol normalization, not a derived result. The scorecard does not predict an exact cross-section, only a band between 5.7 and 7.1 × 10⁻³⁹ cm².
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How does the framework derive the dark matter to neutrino cross-section ratio from its cost function?
- What experimental detector currently has the sensitivity to test the predicted dark matter band?
- How would the scorecard change if a different reference neutrino energy were chosen?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM row_weak_ref_cross_section_band · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
theorem row_weak_ref_cross_section_band : 5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38 := by unfold sigma_nu_weak_ref_cm2 E_ref_GeV gev2_to_cm2 have hgf := row_fermi_pred_bracket have hgf_pos : 0 < row_fermi_pred := by linarith [hgf.1] constructor · nlinarith [hgf.1, hgf_pos] · nlinarith [hgf.2, hgf_pos]The reference value falls between 5.2 × 10⁻³⁸ and 5.4 × 10⁻³⁸ cm². row_weak_ref_cross_section_band · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.leanTHEOREM row_sigma_DM_weak_ref_band · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
theorem row_sigma_DM_weak_ref_band : 5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39 := by unfold sigma_DM_weak_ref_cm2 have href := row_weak_ref_cross_section_band have hratio := row_sigma_ratio_band have href_pos : 0 < sigma_nu_weak_ref_cm2 := by linarith [href.1] have hratio_pos : 0 < sigma_DM_over_sigma_nu_RS := by linarith [hratio.1] constructor · nlinarith [href.1, hratio.1, href_pos, hratio_pos] · nlinarith [href.2, hratio.2, href_pos, hratio_pos]The dark matter band lies between 5.7 × 10⁻³⁹ and 7.1 × 10⁻³⁹ cm². row_sigma_DM_weak_ref_band · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.leanTHEOREM darkMatterWeakReferenceCrossSectionScoreCardCert_holds · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean
theorem darkMatterWeakReferenceCrossSectionScoreCardCert_holds : Nonempty DarkMatterWeakReferenceCrossSectionScoreCardCert := ⟨{ weak_ref_band := row_weak_ref_cross_section_band sigma_dm_band := row_sigma_DM_weak_ref_band fermi_bracket := row_fermi_pred_bracket sigma_ratio_band := row_sigma_ratio_band }⟩The ratio between dark matter and neutrino cross-sections is between 0.11 and 0.13. darkMatterWeakReferenceCrossSectionScoreCardCert_holds · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean