IndisputableMonolith.Cosmology.DarkMatterCrossSectionBound

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Dark Matter Cross-Section Bound from J-Cost
   7
   8The RS dark-matter prediction (`Foundation/DarkMatterConsciousnessIdentity`)
   9identifies the candidate as the consciousness-sector boundary of the
  10Higgs vacuum at `m_DM = m_W / 45 ≈ 1.79 GeV` with direct-detection
  11cross-section `σ_DM = J(φ) · σ_neutrino ≈ 0.118 × 10⁻⁴⁴ cm²`.
  12
  13This module records the structural bound. The cross-section ratio
  14`r := σ_DM / σ_neutrino` equals `J(φ)`, the canonical golden-section
  15J-cost quantum, lying in the band `(0.11, 0.13)`. The cross-section is
  16strictly positive (RS-canonical detection is permitted), and any
  17exclusion at lower cross-section would falsify the identification.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Cosmology
  24namespace DarkMatterCrossSectionBound
  25
  26open Constants Cost
  27
  28noncomputable section
  29
  30/-- The RS-predicted dark-matter cross-section ratio. -/
  31def crossSectionRatio : ℝ := Cost.Jcost phi
  32
  33/-- The cross-section ratio is strictly positive. -/
  34theorem crossSectionRatio_pos : 0 < crossSectionRatio := by
  35  unfold crossSectionRatio
  36  have hphi_ne_one : phi ≠ 1 := by
  37    intro h
  38    have hphi_gt : (1 : ℝ) < phi := by
  39      have := Constants.phi_gt_onePointFive; linarith
  40    rw [h] at hphi_gt
  41    exact lt_irrefl _ hphi_gt
  42  exact Cost.Jcost_pos_of_ne_one phi Constants.phi_pos hphi_ne_one
  43
  44/-- The cross-section ratio sits in the canonical band. -/
  45theorem crossSectionRatio_band :
  46    0.11 < crossSectionRatio ∧ crossSectionRatio < 0.13 := by
  47  unfold crossSectionRatio
  48  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  49  rw [Cost.Jcost_eq_sq hphi_ne]
  50  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  51  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  52  have hpos : (0 : ℝ) < 2 * phi := by
  53    have : (0 : ℝ) < phi := Constants.phi_pos
  54    linarith
  55  refine ⟨?lo, ?hi⟩
  56  · rw [lt_div_iff₀ hpos]
  57    nlinarith [h_lo, h_hi]
  58  · rw [div_lt_iff₀ hpos]
  59    nlinarith [h_lo, h_hi]
  60
  61/-- Detection within the predicted band of cross-section is consistent. -/
  62def IsInPredictedBand (sigma_meas : ℝ) (sigma_nu : ℝ) : Prop :=
  63  0.11 * sigma_nu < sigma_meas ∧ sigma_meas < 0.13 * sigma_nu
  64
  65/-- Exclusion below the predicted band of cross-section is a falsifier. -/
  66def FalsifiesPrediction (sigma_excl : ℝ) (sigma_nu : ℝ) : Prop :=
  67  sigma_excl < 0.11 * sigma_nu
  68
  69/-- Predicted band and exclusion-falsifier are mutually exclusive in the
  70following sense: a measurement σ that simultaneously sits in the
  71predicted band and falsifies the prediction is impossible. -/
  72theorem band_excludes_falsifier {sigma sigma_nu : ℝ} :
  73    ¬ (IsInPredictedBand sigma sigma_nu ∧ FalsifiesPrediction sigma sigma_nu) := by
  74  rintro ⟨⟨h_lo, _⟩, h_excl⟩
  75  exact (lt_irrefl _) (lt_trans h_excl h_lo)
  76
  77structure DarkMatterCrossSectionCert where
  78  ratio_pos : 0 < crossSectionRatio
  79  ratio_band : 0.11 < crossSectionRatio ∧ crossSectionRatio < 0.13
  80  band_excludes_falsifier :
  81    ∀ {sigma sigma_nu : ℝ},
  82      ¬ (IsInPredictedBand sigma sigma_nu ∧ FalsifiesPrediction sigma sigma_nu)
  83
  84/-- Dark-matter-cross-section bound certificate. -/
  85def darkMatterCrossSectionCert : DarkMatterCrossSectionCert where
  86  ratio_pos := crossSectionRatio_pos
  87  ratio_band := crossSectionRatio_band
  88  band_excludes_falsifier := band_excludes_falsifier
  89
  90end
  91end DarkMatterCrossSectionBound
  92end Cosmology
  93end IndisputableMonolith
  94