module module

`IndisputableMonolith.Physics.TopMSBarScoreCard`

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

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension module_import
IndisputableMonolith.Physics.QCDRGE.PoleToMSbar module_import
IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS module_import

declarations in this module (12)

def m_t_pole_PDG_GeV L28
def m_t_pole_PDG_unc_GeV L29
theorem m_t_pole_PDG_pos L31
def r_top L33
def m_t_MS_at_mt_GeV L37
theorem m_t_MS_at_mt_pos L39
def m_t_pole_predicted L43
def m_t_pole_predicted_via_RS L47
theorem m_t_pole_predicted_via_RS_in_PDG_band L49
theorem m_t_pole_predicted_pos L55
structure TopMSBarCert L60
theorem topMSBarCert_holds L69