module module

`IndisputableMonolith.Physics.CharmMSBarScoreCard`

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.ThresholdMatching module_import
IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS module_import

declarations in this module (12)

def m_c_PDG_GeV L37
def m_c_PDG_unc_GeV L40
theorem m_c_PDG_pos L42
def r_charm L47
def m_c_at_MZ_GeV L56
theorem m_c_at_MZ_pos L58
def m_c_predicted L68
def m_c_predicted_via_RS L73
theorem m_c_predicted_via_RS_in_PDG_band L75
theorem m_c_predicted_pos L80
structure CharmMSBarCert L89
theorem charmMSBarCert_holds L97