IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard

   1import Mathlib
   2import IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard
   3
   4/-!
   5# P0-A6 -- absolute cross-section normalization scorecard
   6
   7Row ID: P0-A6-01 absolute cross-section normalization.
   8
   9Predicted formula: `sigma_DM = (sigma_DM/sigma_nu) * sigma_nu_ref`,
  10where `0.11 < sigma_DM/sigma_nu < 0.13` and the current protocol
  11normalization is `sigma_nu_ref = 1e-38 cm^2`.
  12
  13Measurement/protocol target: detector-limit comparisons should use the
  14derived band `(1.1e-39, 1.3e-39) cm^2` only after a sub-0.35 keV
  15efficiency curve is supplied.
  16
  17Falsifier: a detector with valid efficiency at or below 0.35 keV
  18excluding `sigma_DM ∈ (1.1e-39, 1.3e-39) cm^2` falsifies P0-A6 under
  19this normalization.
  20
  21Status: PARTIAL_THEOREM / HYPOTHESIS. The absolute band follows from a
  22named protocol normalization; deriving that normalization from RS
  23or a specified neutrino channel remains open.
  24
  25Lean: 0 sorry, 0 new axiom.
  26-/
  27
  28namespace IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard
  29
  30open IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard
  31
  32noncomputable section
  33
  34/-- Protocol normalization for the neutrino-reference channel in cm^2. -/
  35def sigma_nu_reference_cm2 : ℝ := 1e-38
  36
  37/-- Absolute dark-matter cross-section prediction in cm^2. -/
  38def sigma_DM_cm2 : ℝ := sigma_DM_over_sigma_nu_RS * sigma_nu_reference_cm2
  39
  40theorem row_sigma_nu_reference_pos : 0 < sigma_nu_reference_cm2 := by
  41  unfold sigma_nu_reference_cm2
  42  norm_num
  43
  44theorem row_sigma_DM_cm2_band :
  45    1.1e-39 < sigma_DM_cm2 ∧ sigma_DM_cm2 < 1.3e-39 := by
  46  unfold sigma_DM_cm2 sigma_nu_reference_cm2
  47  have h := row_sigma_ratio_band
  48  constructor
  49  · nlinarith [h.1]
  50  · nlinarith [h.2]
  51
  52structure DarkMatterAbsoluteCrossSectionScoreCardCert where
  53  sigma_nu_ref_pos : 0 < sigma_nu_reference_cm2
  54  sigma_ratio_band :
  55    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13
  56  sigma_absolute_band : 1.1e-39 < sigma_DM_cm2 ∧ sigma_DM_cm2 < 1.3e-39
  57
  58theorem darkMatterAbsoluteCrossSectionScoreCardCert_holds :
  59    Nonempty DarkMatterAbsoluteCrossSectionScoreCardCert :=
  60  ⟨{ sigma_nu_ref_pos := row_sigma_nu_reference_pos
  61     sigma_ratio_band := row_sigma_ratio_band
  62     sigma_absolute_band := row_sigma_DM_cm2_band }⟩
  63
  64end
  65
  66end IndisputableMonolith.Physics.DarkMatterAbsoluteCrossSectionScoreCard
  67