IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# P0-A6 -- dark-matter cross-section ratio band
   6
   7Row ID: P0-A6-01 cross-section structural band.
   8
   9Predicted formula: the native dark-matter cross-section ratio to the
  10neutrino reference channel is the golden-section recognition quantum
  11`J(phi) = phi - 3/2`.
  12
  13Measurement/protocol target: direct-detection exclusion curves must be
  14compared against this band after detector threshold and efficiency are
  15locked. This file proves the RS-native ratio band only.
  16
  17Falsifier: a detector with sufficient sub-keV reach excluding the
  18cross-section ratio band `(0.11,0.13)` under the locked normalization
  19falsifies the P0-A6 direct-detection claim.
  20
  21Status: PARTIAL_THEOREM / HYPOTHESIS. The native ratio band builds;
  22absolute cross-section normalization and detector-efficiency curves
  23remain empirical.
  24
  25Lean: 0 sorry, 0 new axiom.
  26-/
  27
  28namespace IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard
  29
  30open IndisputableMonolith.Constants
  31
  32noncomputable section
  33
  34/-- Native cross-section ratio, `sigma_DM / sigma_nu = J(phi)`. -/
  35def sigma_DM_over_sigma_nu_RS : ℝ := phi - 3 / 2
  36
  37theorem row_sigma_ratio_pos : 0 < sigma_DM_over_sigma_nu_RS := by
  38  unfold sigma_DM_over_sigma_nu_RS
  39  linarith [phi_gt_onePointSixOne]
  40
  41theorem row_sigma_ratio_band :
  42    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13 := by
  43  unfold sigma_DM_over_sigma_nu_RS
  44  constructor
  45  · linarith [phi_gt_onePointSixOne]
  46  · linarith [phi_lt_onePointSixTwo]
  47
  48structure DarkMatterCrossSectionBandScoreCardCert where
  49  sigma_ratio_pos : 0 < sigma_DM_over_sigma_nu_RS
  50  sigma_ratio_band :
  51    0.11 < sigma_DM_over_sigma_nu_RS ∧ sigma_DM_over_sigma_nu_RS < 0.13
  52
  53theorem darkMatterCrossSectionBandScoreCardCert_holds :
  54    Nonempty DarkMatterCrossSectionBandScoreCardCert :=
  55  ⟨{ sigma_ratio_pos := row_sigma_ratio_pos
  56     sigma_ratio_band := row_sigma_ratio_band }⟩
  57
  58end
  59
  60end IndisputableMonolith.Physics.DarkMatterCrossSectionBandScoreCard
  61