IndisputableMonolith.Physics.DarkMatterHaloProfileFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Dark Matter Halo Profile from RS — A6 Depth
   6
   7Five canonical dark-matter halo regimes (= configDim D = 5):
   8  NFW inner, NFW outer, Einasto profile, isothermal sphere, truncation edge.
   9
  10Each regime sits one rung down the φ-ladder in density.
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Physics.DarkMatterHaloProfileFromRS
  16open Constants
  17
  18inductive HaloRegime where
  19  | nfwInner
  20  | nfwOuter
  21  | einasto
  22  | isothermal
  23  | truncation
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem haloRegime_count : Fintype.card HaloRegime = 5 := by decide
  27
  28noncomputable def densityRung (k : ℕ) : ℝ := 1 / phi ^ k
  29
  30theorem density_pos (k : ℕ) : 0 < densityRung k := by
  31  unfold densityRung
  32  exact div_pos one_pos (pow_pos phi_pos k)
  33
  34theorem density_strictDecr (k : ℕ) :
  35    densityRung (k + 1) < densityRung k := by
  36  unfold densityRung
  37  have hpos_k : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  38  have h_growth : phi ^ k < phi ^ (k + 1) := by
  39    rw [pow_succ]
  40    have h1 : 1 < phi := one_lt_phi
  41    nlinarith
  42  exact one_div_lt_one_div_of_lt hpos_k h_growth
  43
  44structure DarkMatterHaloCert where
  45  five_regimes : Fintype.card HaloRegime = 5
  46  density_always_pos : ∀ k, 0 < densityRung k
  47  density_strictly_decreasing : ∀ k, densityRung (k + 1) < densityRung k
  48
  49noncomputable def darkMatterHaloCert : DarkMatterHaloCert where
  50  five_regimes := haloRegime_count
  51  density_always_pos := density_pos
  52  density_strictly_decreasing := density_strictDecr
  53
  54end IndisputableMonolith.Physics.DarkMatterHaloProfileFromRS
  55