nuclear_efficiency_valid

formal source

  30def nuclear_efficiency : ℝ := 0.007
  31
  32/-- Nuclear efficiency is positive and less than 1. -/
  33theorem nuclear_efficiency_valid :
  34    0 < nuclear_efficiency ∧ nuclear_efficiency < 1 := by
  35  norm_num [nuclear_efficiency]
  36
  37/-- **GAMOW ENERGY**: peak of energy window for nuclear reactions.
  38    E_Gamow = (π η_G k_B T)^{2/3} / E_keV
  39    The pp chain dominates at T ~ 10⁷ K (solar core temperature). -/
  40noncomputable def gamow_energy (T Z₁Z₂ μ : ℝ) : ℝ :=
  41  -- In keV: E_G = 1.22 × (Z₁Z₂)² × μ × (T/10⁷K)^{2/3} keV
  42  1.22 * Z₁Z₂^2 * μ * (T / 1e7) ^ ((2:ℝ)/3)
  43
  44/-- Gamow energy scales as T^{2/3}. -/
  45theorem gamow_energy_increases_with_T (Z₁Z₂ μ T₁ T₂ : ℝ)
  46    (hZ : 0 < Z₁Z₂) (hμ : 0 < μ) (hT₁ : 0 < T₁) (h : T₁ < T₂) :
  47    gamow_energy T₁ Z₁Z₂ μ < gamow_energy T₂ Z₁Z₂ μ := by
  48  unfold gamow_energy
  49  apply mul_lt_mul_of_pos_left _ (by positivity)
  50  apply Real.rpow_lt_rpow (by positivity) (div_lt_div_of_pos_right h (by norm_num)) (by norm_num)
  51
  52/-! ## Stellar Structure Scaling Relations -/
  53
  54/-- **VIRIAL TEMPERATURE**: T_c ∝ GM m_p / (k_B R)
  55    From the virial theorem applied to a stellar interior. -/
  56noncomputable def virial_temperature (M R : ℝ) : ℝ :=
  57  M / R  -- in natural units where G m_p / k_B = 1
  58
  59/-- Central temperature increases with mass for fixed radius. -/
  60theorem temp_increases_with_mass (M₁ M₂ R : ℝ)
  61    (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) (hR : 0 < R) (h : M₁ < M₂) :
  62    virial_temperature M₁ R < virial_temperature M₂ R := by
  63  unfold virial_temperature