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
darkMatterWeakReferenceCrossSectionScoreCardCert_holds · IndisputableMonolith/Physics/DarkMatterWeakReferenceCrossSectionScoreCard.lean:84
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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND