IndisputableMonolith.StandardModel.HiggsEFTBridge

declarations in this module (18)

• def V_RS L67
• theorem V_RS_eq_cosh L70
• theorem V_RS_at_vacuum L76
• theorem V_RS_nonneg L81
• def V_RS_quartic L91
• theorem exp_sub_trunc6_le L99
• theorem cosh_quartic_error L115
• theorem jcost_quartic_error L142
• theorem V_RS_quartic_error L156
• def quadratic_coefficient L176
• def quartic_coefficient_canonical L179
• theorem V_RS_quartic_canonical L183
• def NormalizationHypothesis L201
• theorem mass_term_matches_SM L206
• theorem quartic_coupling_from_normalization L220
• structure HiggsEFTBridgeCert L238
• def higgsEFTBridgeCert L262
• theorem higgsEFTBridgeCert_inhabited L271