beta0QCD_nf0

formal source

 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]
 145
 146/-! ## RK4 integrator scaffold with enclosure bounds -/
 147
 148/-- RK4 increment from stage values `(k1,k2,k3,k4)`. -/
 149def rk4Increment (h k1 k2 k3 k4 : ℝ) : ℝ :=
 150  (h / 6) * (k1 + 2 * k2 + 2 * k3 + k4)
 151
 152/-- One RK4 step for `x' = f(x)` with step size `h`. -/
 153def rk4Step (f : ℝ → ℝ) (x h : ℝ) : ℝ :=
 154  let k1 := f x
 155  let k2 := f (x + (h / 2) * k1)
 156  let k3 := f (x + (h / 2) * k2)