module module

`IndisputableMonolith.Physics.WBosonAbsoluteScoreCard`

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.VEVConsistency module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import

declarations in this module (13)

theorem cos2_theta_W_closed_form L42
theorem cos2_gt L48
theorem cos2_lt L60
theorem sin2_gt L66
theorem sin2_lt L72
theorem cos2_pos L84
theorem wz_ratio_is_cos_theta L87
def free_params_w_mass L92
theorem zero_free_params L93
inductive WMassInput L96
theorem three_inputs L102
structure WBosonAbsoluteScoreCardCert L104
theorem wBosonAbsoluteScoreCardCert_holds L112