structure
definition
TwoLoopAlphaSCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS on GitHub at line 123.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
120
121/-! ## Master cert -/
122
123structure TwoLoopAlphaSCert where
124 /-- One-loop coefficient is positive at N_f = 5. -/
125 b0_at5_pos : 0 < b0 5
126 /-- Two-loop coefficient is positive at N_f = 5. -/
127 b1_at5_pos : 0 < b1 5
128 /-- The running formula reduces to identity at the anchor scale. -/
129 reduces_at_anchor : ∀ (alpha_0 : ℝ) (N_f : ℕ) (mu_0_GeV : ℝ),
130 0 < mu_0_GeV → alpha_s_two_loop alpha_0 N_f mu_0_GeV mu_0_GeV = alpha_0
131
132theorem twoLoopAlphaSCert_holds : TwoLoopAlphaSCert :=
133 { b0_at5_pos := b0_at_Nf5_pos
134 b1_at5_pos := b1_at_Nf5_pos
135 reduces_at_anchor := alpha_s_two_loop_at_anchor }
136
137end
138
139end IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS