module module

`IndisputableMonolith.Physics.GaugeCouplingHierarchyScoreCard`

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.Constants.StrongCoupling module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import
IndisputableMonolith.Numerics.Interval.W8Bounds module_import

declarations in this module (12)

def sin2_W_rs L29
theorem sin2_W_pos L32
theorem sin2_W_lt_one L41
def alpha_weak_inv L54
theorem em_exceeds_weak L57
theorem alpha_inv_em_band L64
theorem gauge_sum_12pi L69
theorem alpha_s_pos L73
def free_params L76
theorem zero_free_params L77
structure GaugeCouplingHierarchyScoreCardCert L79
theorem gaugeCouplingHierarchyScoreCardCert_holds L88