module module

`IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS`

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

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.BottomMSBarScoreCard module_import
IndisputableMonolith.Physics.CharmMSBarScoreCard module_import
IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension module_import
IndisputableMonolith.Physics.QCDRGE.PoleToMSbar module_import
IndisputableMonolith.Physics.QCDRGE.ThresholdMatching module_import
IndisputableMonolith.Physics.TopMSBarScoreCard module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Physics.QCDRGE.AlphaRunning module_import
IndisputableMonolith.Physics.StrongForce module_import

declarations in this module (13)

def N_c L41
def C_F L44
def b0 L47
def b1 L50
theorem b1_pos_lowNf L54
theorem b1_at_Nf5_pos L61
theorem b0_at_Nf5_pos L64
def alpha_s_two_loop L70
theorem alpha_s_two_loop_b1_zero_eq_one_loop L79
theorem alpha_s_two_loop_pos_when_denom_pos L92
theorem alpha_s_two_loop_at_anchor L111
structure TwoLoopAlphaSCert L123
theorem twoLoopAlphaSCert_holds L132