module module

`IndisputableMonolith.Physics.AlphaRunningCorrectionScoreCard`

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 (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.VEVConsistency module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import

declarations in this module (14)

def alpha_inv_0 L37
def alpha_inv_mz_pdg L40
def running_ratio L43
theorem alpha_inv_0_gt L46
theorem alpha_inv_0_lt L50
theorem running_ratio_lt_one L54
theorem running_ratio_gt L60
theorem running_ratio_lt L68
def n_charged_leptons L76
def n_light_quarks L79
def particle_content_free_params L82
theorem zero_free_params L83
structure AlphaRunningCorrectionScoreCardCert L85
theorem alphaRunningCorrectionScoreCardCert_holds L93