alpha_unmatch

formal source

 103/-- The matching at any threshold is a multiplicative perturbation; its inverse
 104    factor at NLO is `1 - c_2_alpha * (a/pi)^2 + O(a^4)`. We expose this as a
 105    structural definition rather than re-proving the perturbative inverse. -/
 106def alpha_unmatch (alpha_below : ℝ) : ℝ :=
 107  alpha_below * (1 - c_2_alpha * (alpha_below / Real.pi) ^ 2)
 108
 109/-! ## Master cert -/
 110
 111structure ThresholdMatchingCert where
 112  c_2_alpha_pos : 0 < c_2_alpha
 113  d_2_mass_neg : d_2_mass < 0
 114  alpha_match_pos_lemma : ∀ alpha_above : ℝ,
 115      0 < alpha_above → alpha_above < 1 → 0 < alpha_match alpha_above
 116  mass_match_pos_lemma : ∀ mass_above alpha_at_threshold : ℝ,
 117      0 < mass_above → 0 < alpha_at_threshold → alpha_at_threshold < 1 →
 118      0 < mass_match mass_above alpha_at_threshold
 119
 120theorem c_2_alpha_pos : 0 < c_2_alpha := by unfold c_2_alpha; norm_num
 121theorem d_2_mass_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
 122
 123theorem thresholdMatchingCert_holds : ThresholdMatchingCert :=
 124  { c_2_alpha_pos := c_2_alpha_pos
 125    d_2_mass_neg := d_2_mass_neg
 126    alpha_match_pos_lemma := alpha_match_pos
 127    mass_match_pos_lemma := mass_match_pos }
 128
 129end
 130
 131end IndisputableMonolith.Physics.QCDRGE.ThresholdMatching