betaQED1L

formal source

 111
 112/-- One-loop QED running with an effective charge-weight factor.
 113This keeps the kernel explicit while allowing policy-level charge sums. -/
 114noncomputable def betaQED1L (chargeWeight : ℝ) (alpha : ℝ) : ℝ :=
 115  (chargeWeight / (3 * Real.pi)) * alpha ^ 2
 116
 117/-- Minimal one-loop mass anomalous-dimension scaffold for QCD.
 118The exact scheme-dependent higher-loop expression is left to Level-B extensions. -/
 119noncomputable def gammaMassQCD1L (alphaS : ℝ) : ℝ :=
 120  (2 / Real.pi) * alphaS
 121
 122/-- Minimal one-loop mass anomalous-dimension scaffold for QED. -/
 123noncomputable def gammaMassQED1L (chargeSq : ℝ) (alpha : ℝ) : ℝ :=
 124  (3 * chargeSq / (4 * Real.pi)) * alpha
 125
 126theorem beta0QCD_nf0 : beta0QCD 0 = 11 := by
 127  norm_num [beta0QCD]
 128
 129theorem beta0QCD_asymp_free (nf : ℕ) (hnf : nf ≤ 16) : 0 < beta0QCD nf := by
 130  unfold beta0QCD
 131  have hnfQ : (nf : ℚ) ≤ 16 := by
 132    exact_mod_cast hnf
 133  have h_le : (2 : ℚ) * nf / 3 ≤ (2 : ℚ) * 16 / 3 := by
 134    exact div_le_div_of_nonneg_right (by nlinarith [hnfQ]) (by norm_num)
 135  have h_lt : (2 : ℚ) * 16 / 3 < 11 := by norm_num
 136  have h_frac_lt : (2 : ℚ) * nf / 3 < 11 := lt_of_le_of_lt h_le h_lt
 137  linarith
 138
 139theorem betaQCD1L_vanishes_at_zero (nf : ℕ) :
 140    betaQCD1L nf 0 = 0 := by
 141  simp [betaQCD1L]
 142
 143theorem gammaMassQCD1L_zero : gammaMassQCD1L 0 = 0 := by
 144  simp [gammaMassQCD1L]