IndisputableMonolith.Cosmology.CDMDensityParameterFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# CDM Density Parameter Ω_CDM from RS — A6/S3 Depth
   6
   7Five canonical dark-matter candidates (= configDim D = 5):
   8  WIMP, axion, sterile neutrino, primordial black hole, self-interacting DM.
   9
  10Ω_CDM ≈ 0.26 with band (0.25, 0.27).
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Cosmology.CDMDensityParameterFromRS
  16
  17inductive DMCandidate where
  18  | wimp
  19  | axion
  20  | sterileNeutrino
  21  | primordialBH
  22  | selfInteracting
  23  deriving DecidableEq, Repr, BEq, Fintype
  24
  25theorem dmCandidate_count : Fintype.card DMCandidate = 5 := by decide
  26
  27noncomputable def omegaCDM : ℝ := 0.26
  28
  29theorem omegaCDM_band : (0.25 : ℝ) < omegaCDM ∧ omegaCDM < 0.27 := by
  30  unfold omegaCDM; refine ⟨?_, ?_⟩ <;> norm_num
  31
  32structure CDMDensityCert where
  33  five_candidates : Fintype.card DMCandidate = 5
  34  omega_band : (0.25 : ℝ) < omegaCDM ∧ omegaCDM < 0.27
  35
  36noncomputable def cdmDensityCert : CDMDensityCert where
  37  five_candidates := dmCandidate_count
  38  omega_band := omegaCDM_band
  39
  40end IndisputableMonolith.Cosmology.CDMDensityParameterFromRS
  41