IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants.FermiConstantScoreCard
   3import IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard
   4
   5/-!
   6# P0-A6 -- weak neutrino-reference cross-section scorecard
   7
   8Row ID: P0-A6-01 weak reference channel.
   9
  10Predicted/reference formula:
  11
  12`sigma_nu_ref = G_F^2 * E_ref^2 * (GeV^-2 -> cm^2)`,
  13
  14with `E_ref = 1 GeV` and conversion factor `0.3894e-27 cm^2/GeV^-2`.
  15
  16Measurement/protocol target: this names the neutrino reference channel
  17used by the P0-A6 cross-section ratio.  It gives
  18`5.2e-38 < sigma_nu_ref < 5.4e-38 cm^2`, hence
  19`5.7e-39 < sigma_DM < 7.1e-39 cm^2` from `J(phi)`.
  20
  21Falsifier: if the named weak reference channel is not the intended
  22detector normalization, this row must be replaced; if it is the
  23normalization, a sub-0.35 keV detector excluding the derived band
  24falsifies P0-A6.
  25
  26Status: PARTIAL_THEOREM / HYPOTHESIS. The arithmetic follows from the
  27Fermi scorecard; the choice of a 1 GeV weak reference channel remains
  28a protocol normalization.
  29
  30Lean: 0 sorry, 0 new axiom.
  31-/
  32
  33namespace IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard
  34
  35open IndisputableMonolith.Constants.FermiConstantScoreCard
  36open IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard
  37
  38noncomputable section
  39
  40/-- Reference neutrino energy for the weak-channel normalization, in GeV. -/
  41def E_ref_GeV : ℝ := 1
  42
  43/-- Conversion `1 GeV^-2 = 0.3894e-27 cm^2`. -/
  44def gev2_to_cm2 : ℝ := 0.3894e-27
  45
  46/-- Named weak-channel reference cross-section in cm^2. -/
  47def sigma_nu_weak_ref_cm2 : ℝ :=
  48  row_fermi_pred ^ (2 : ℕ) * E_ref_GeV ^ (2 : ℕ) * gev2_to_cm2
  49
  50/-- Derived absolute dark-matter cross-section in cm^2 on this reference. -/
  51def sigma_DM_weak_ref_cm2 : ℝ :=
  52  sigma_DM_over_sigma_nu_RS * sigma_nu_weak_ref_cm2
  53
  54theorem row_weak_ref_cross_section_band :
  55    5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38 := by
  56  unfold sigma_nu_weak_ref_cm2 E_ref_GeV gev2_to_cm2
  57  have hgf := row_fermi_pred_bracket
  58  have hgf_pos : 0 < row_fermi_pred := by linarith [hgf.1]
  59  constructor
  60  · nlinarith [hgf.1, hgf_pos]
  61  · nlinarith [hgf.2, hgf_pos]
  62
  63theorem row_sigma_DM_weak_ref_band :
  64    5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39 := by
  65  unfold sigma_DM_weak_ref_cm2
  66  have href := row_weak_ref_cross_section_band
  67  have hratio := row_sigma_ratio_band
  68  have href_pos : 0 < sigma_nu_weak_ref_cm2 := by linarith [href.1]
  69  have hratio_pos : 0 < sigma_DM_over_sigma_nu_RS := by linarith [hratio.1]
  70  constructor
  71  · nlinarith [href.1, hratio.1, href_pos, hratio_pos]
  72  · nlinarith [href.2, hratio.2, href_pos, hratio_pos]
  73
  74structure DarkMatterWeakReferenceCrossSectionScoreCardCert where
  75  weak_ref_band :
  76    5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38
  77  sigma_dm_band :
  78    5.7e-39 < sigma_DM_weak_ref_cm2 ∧ sigma_DM_weak_ref_cm2 < 7.1e-39
  79  fermi_bracket :
  80    (1.16e-5 : ℝ) < row_fermi_pred ∧ row_fermi_pred < (1.17e-5 : ℝ)
  81  sigma_ratio_band :
  82    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13
  83
  84theorem darkMatterWeakReferenceCrossSectionScoreCardCert_holds :
  85    Nonempty DarkMatterWeakReferenceCrossSectionScoreCardCert :=
  86  ⟨{ weak_ref_band := row_weak_ref_cross_section_band
  87     sigma_dm_band := row_sigma_DM_weak_ref_band
  88     fermi_bracket := row_fermi_pred_bracket
  89     sigma_ratio_band := row_sigma_ratio_band }⟩
  90
  91end
  92
  93end IndisputableMonolith.Physics.DarkMatterWeakReferenceCrossSectionScoreCard
  94