`mass_evolution_exp`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.RunningCouplings
domain: Physics
line: 244 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.RunningCouplings on GitHub at line 244.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 241def mass_anomalous_dim : ℝ := 8
 242
 243/-- Mass evolution exponent γ₀/(2b₀) for `n_f` active flavors. -/
 244noncomputable def mass_evolution_exp (n_f : ℕ) : ℝ :=
 245  mass_anomalous_dim / (2 * b0_qcd n_f)
 246
 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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.