def
definition
running_mass
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.RunningCouplings on GitHub at line 268.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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. -/
281structure FlavorThreshold where
282 scale : ℝ
283 n_f_below : ℕ
284 n_f_above : ℕ
285 h_pos : 0 < scale
286 h_step : n_f_below + 1 = n_f_above
287
288def charm_threshold : FlavorThreshold where
289 scale := 1.27
290 n_f_below := 3
291 n_f_above := 4
292 h_pos := by norm_num
293 h_step := by norm_num
294
295def bottom_threshold : FlavorThreshold where
296 scale := 4.18
297 n_f_below := 4
298 n_f_above := 5