inv_pole_factor_at_zero

formal source

  82    (i.e., differs only by terms of order `alpha_s^3` or higher), but we do
  83    not state that algebraic identity explicitly here; it is straightforward
  84    algebra and not used in the downstream scorecards. -/
  85theorem inv_pole_factor_at_zero (N_l : ℕ) :
  86    inv_pole_factor 0 N_l = 1 := by
  87  unfold inv_pole_factor
  88  simp
  89
  90/-! ## Master cert -/
  91
  92structure PoleToMSbarCert where
  93  K_1_eq : K_1 = 4 / 3
  94  K_2_at5_pos : 0 < K_2 5
  95  pole_factor_pos_lemma : ∀ alpha_s : ℝ,
  96      0 < alpha_s → alpha_s < 0.5 → 0 < pole_factor alpha_s 5
  97  m_pole_pos_lemma : ∀ m_MS alpha_s : ℝ,
  98      0 < m_MS → 0 < alpha_s → alpha_s < 0.5 →
  99      0 < m_pole_from_MS m_MS alpha_s 5
 100
 101theorem K_2_at5_pos : 0 < K_2 5 := by unfold K_2; norm_num
 102
 103theorem poleToMSbarCert_holds : PoleToMSbarCert :=
 104  { K_1_eq := rfl
 105    K_2_at5_pos := K_2_at5_pos
 106    pole_factor_pos_lemma := pole_factor_pos_top
 107    m_pole_pos_lemma := m_pole_from_MS_pos_top }
 108
 109end
 110
 111end IndisputableMonolith.Physics.QCDRGE.PoleToMSbar