mass_evolution_exp_pos

formal source

 247theorem mass_anomalous_dim_pos : 0 < mass_anomalous_dim := by
 248  unfold mass_anomalous_dim; norm_num
 249
 250theorem mass_evolution_exp_pos (n_f : ℕ) (h : n_f ≤ 16) :
 251    0 < mass_evolution_exp n_f := by
 252  unfold mass_evolution_exp
 253  exact div_pos mass_anomalous_dim_pos
 254    (mul_pos (by norm_num) (asymptotic_freedom_criterion n_f h))
 255
 256/-- Concrete mass evolution exponents for physical n_f values. -/
 257theorem mass_evo_exp_nf3 : mass_evolution_exp 3 = 8 / 18 := by
 258  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 259theorem mass_evo_exp_nf4 : mass_evolution_exp 4 = 8 / (50 / 3) := by
 260  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 261theorem mass_evo_exp_nf5 : mass_evolution_exp 5 = 8 / (46 / 3) := by
 262  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 263theorem mass_evo_exp_nf6 : mass_evolution_exp 6 = 8 / 14 := by
 264  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 265
 266/-- LO QCD running mass at scale μ₂ given reference mass at μ₁.
 267    Uses real-valued power `rpow` since the exponent γ₀/(2b₀) is non-integer. -/
 268noncomputable def running_mass (m_ref α_s_ref α_s_target : ℝ) (n_f : ℕ) : ℝ :=
 269  m_ref * (α_s_target / α_s_ref) ^ (mass_evolution_exp n_f)
 270
 271/-- **Mass ratios within a sector are RG-invariant at LO** when both masses
 272    are evolved from the same reference scale with the same α_s values. -/
 273theorem mass_ratio_rg_invariant (m1 m2 α_s_ref α_s_target : ℝ) (n_f : ℕ)
 274    (hr : (α_s_target / α_s_ref) ^ (mass_evolution_exp n_f) ≠ 0) :
 275    running_mass m1 α_s_ref α_s_target n_f / running_mass m2 α_s_ref α_s_target n_f =
 276    m1 / m2 := by
 277  unfold running_mass
 278  rw [mul_div_mul_right _ _ hr]
 279
 280/-- SM flavor threshold data. -/