def
definition
M_Z_GeV
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QCDRGE.AlphaRunning on GitHub at line 53.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
50 unfold alpha_s_MZ alpha_s_geom; constructor <;> norm_num
51
52/-- Z boson mass in GeV. -/
53def M_Z_GeV : ℝ := 91.1876
54
55/-- Running α_s at scale Q (one-loop). -/
56def alpha_s_running (Q_GeV : ℝ) : ℝ :=
57 alpha_s_MZ / (1 + beta0 N_f_Z * alpha_s_MZ * Real.log (Q_GeV ^ 2 / M_Z_GeV ^ 2) / (2 * Real.pi))
58
59/-- For Q < M_Z, ln(Q²/M_Z²) < 0, so α_s increases (asymptotic freedom in reverse). -/
60theorem low_Q_log_negative (Q : ℝ) (hQ : 0 < Q) (h : Q < M_Z_GeV) :
61 Real.log (Q ^ 2 / M_Z_GeV ^ 2) < 0 := by
62 apply Real.log_neg
63 · apply div_pos (sq_pos_of_pos hQ)
64 exact sq_pos_of_pos (by unfold M_Z_GeV; norm_num)
65 · rw [div_lt_one (by unfold M_Z_GeV; positivity)]
66 nlinarith [sq_nonneg Q, sq_nonneg M_Z_GeV, sq_abs (Q - M_Z_GeV)]
67
68/-- At Q = M_Z the log vanishes so α_s = α_s(M_Z). -/
69theorem log_at_MZ : Real.log (M_Z_GeV ^ 2 / M_Z_GeV ^ 2) = 0 := by
70 rw [div_self (by unfold M_Z_GeV; positivity)]; exact Real.log_one
71
72/-- Asymptotic freedom: α_s gets STRONGER at lower energies. -/
73theorem asymptotic_freedom :
74 0 < beta0 N_f_Z := beta0_pos N_f_Z (by unfold N_f_Z; norm_num)
75
76end
77
78end AlphaRunning
79end QCDRGE
80end Physics
81end IndisputableMonolith