IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Neutron Star Crustal Regimes from RS — Astrophysics Depth
   6
   7Five canonical neutron-star crustal regimes (= configDim D = 5):
   8  outer crust, inner crust, nuclear pasta, outer core, inner core.
   9
  10Density rung on the φ-ladder: adjacent-regime density ratio = φ.
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS
  16open Constants
  17
  18inductive NSRegime where
  19  | outerCrust
  20  | innerCrust
  21  | nuclearPasta
  22  | outerCore
  23  | innerCore
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem nsRegime_count : Fintype.card NSRegime = 5 := by decide
  27
  28noncomputable def density (k : ℕ) : ℝ := phi ^ k
  29
  30theorem density_ratio (k : ℕ) : density (k + 1) / density k = phi := by
  31  unfold density
  32  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  33  rw [div_eq_iff hpos.ne', pow_succ]
  34  ring
  35
  36theorem density_pos (k : ℕ) : 0 < density k := pow_pos phi_pos k
  37
  38structure NeutronStarCert where
  39  five_regimes : Fintype.card NSRegime = 5
  40  phi_ratio : ∀ k, density (k + 1) / density k = phi
  41  density_always_pos : ∀ k, 0 < density k
  42
  43noncomputable def neutronStarCert : NeutronStarCert where
  44  five_regimes := nsRegime_count
  45  phi_ratio := density_ratio
  46  density_always_pos := density_pos
  47
  48end IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS
  49