module module

`IndisputableMonolith.Physics.ElectroweakZeroParamScoreCard`

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

Lean names referenced from this declaration's body.

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

declarations in this module (13)

def sm_ew_param_count L37
def rs_ew_param_count L40
inductive EWForcingInput L43
theorem four_forcing_inputs L50
inductive EWSourceTheorem L53
theorem four_source_theorems L60
theorem alpha_in_band L63
theorem sc_product L67
theorem sc_positive L71
theorem rs_zero L75
theorem sm_reduction L78
structure ElectroweakZeroParamScoreCardCert L81
theorem electroweakZeroParamScoreCardCert_holds L91