IndisputableMonolith.Physics.GammaRayBursts

   1import Mathlib
   2import IndisputableMonolith.Cost.JcostCore
   3
   4/-!
   5# Gamma-Ray Bursts from Recognition Science
   6Paper: `RS_Gamma_Ray_Bursts.tex`
   7-/
   8
   9namespace IndisputableMonolith
  10namespace Physics
  11namespace GRB
  12
  13open Real
  14
  15/-! ## GRB Energy Scale -/
  16
  17noncomputable def solar_mass_energy : ℝ := 1.8e54
  18noncomputable def accretion_efficiency : ℝ := 0.1
  19
  20noncomputable def grb_energy (M_frac : ℝ) : ℝ :=
  21  accretion_efficiency * M_frac * solar_mass_energy
  22
  23theorem grb_energy_positive (M_frac : ℝ) (hM : 0 < M_frac) : 0 < grb_energy M_frac := by
  24  unfold grb_energy accretion_efficiency solar_mass_energy; positivity
  25
  26noncomputable def typical_grb_energy : ℝ := grb_energy 0.1
  27
  28theorem typical_grb_in_range :
  29    1e51 < typical_grb_energy ∧ typical_grb_energy < 1e54 := by
  30  simp only [typical_grb_energy, grb_energy, accretion_efficiency, solar_mass_energy]
  31  norm_num
  32
  33/-! ## Two-Class Distinction -/
  34
  35theorem classes_disjoint (x : ℝ)
  36    (hlong : 2 ≤ x) (hshort : x ≤ 2) : x = 2 := le_antisymm hshort hlong
  37
  38theorem long_not_short (x : ℝ) (hlong : 2 < x) (hshort : x < 2) : False := by linarith
  39
  40/-! ## Lorentz Factor -/
  41
  42theorem lorentz_range : (100 : ℝ) < 1000 := by norm_num
  43
  44noncomputable def lorentz_factor (E_jet M_b : ℝ) : ℝ := E_jet / M_b
  45
  46theorem lorentz_positive (E_jet M_b : ℝ) (hE : 0 < E_jet) (hM : 0 < M_b) :
  47    0 < lorentz_factor E_jet M_b := div_pos hE hM
  48
  49/-! ## Amati Relation -/
  50
  51noncomputable def amati_peak (E_iso C : ℝ) : ℝ := C * E_iso ^ ((0.5 : ℝ))
  52
  53theorem amati_increases (E₁ E₂ C : ℝ) (hE₁ : 0 < E₁) (hC : 0 < C) (h : E₁ < E₂) :
  54    amati_peak E₁ C < amati_peak E₂ C := by
  55  unfold amati_peak
  56  apply mul_lt_mul_of_pos_left _ hC
  57  exact Real.rpow_lt_rpow (le_of_lt hE₁) h (by norm_num)
  58
  59/-- Amati exponent 1/2 from Γ ∝ E_iso^(1/4) × √(E_iso) combination. -/
  60theorem amati_exponent : (1:ℝ)/4 + 1/4 = 1/2 := by norm_num
  61
  62/-! ## Key Energy Scale -/
  63
  64/-- GRB isotropic energy: 10^51 to 10^54 erg. -/
  65theorem grb_energy_range :
  66    ∃ E : ℝ, 1e51 < E ∧ E < 1e54 :=
  67  ⟨typical_grb_energy, typical_grb_in_range.1, typical_grb_in_range.2⟩
  68
  69end GRB
  70end Physics
  71end IndisputableMonolith
  72