pith. machine review for the scientific record. sign in
theorem proved term proof

alpha_s_two_loop_b1_zero_eq_one_loop

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  79theorem alpha_s_two_loop_b1_zero_eq_one_loop
  80    (alpha_0 : ℝ) (mu_GeV mu_0_GeV : ℝ) :
  81    1 + b0 5 * alpha_0 * Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2) +
  82        0 * alpha_0 * Real.log (1 + b0 5 * alpha_0 *
  83                                Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2)) =
  84    1 + (11 * (N_c : ℝ) - 2 * 5) / (12 * Real.pi) * alpha_0 *
  85        Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2) := by

proof body

Term-mode proof.

  86  unfold b0 N_c
  87  ring
  88
  89/-- Positivity of the two-loop alpha_s under the MS-bar perturbative window:
  90    when the alpha_0 input is positive and the log scale ratio is bounded
  91    so the denominator stays positive, the running coupling is positive. -/

depends on (15)

Lean names referenced from this declaration's body.