module module

`IndisputableMonolith.StandardModel.HiggsCoshBSMPredictions`

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.Cost module_import
IndisputableMonolith.StandardModel.HiggsEFTBridge module_import

declarations in this module (17)

def V_cosh L89
def V_SM L93
theorem V_cosh_is_even L99
theorem V_SM_at_one L105
theorem V_SM_at_neg_one L110
theorem V_SM_difference_not_zero L116
theorem V_cosh_neq_V_SM L127
def kappa_lambda_3_RS L162
theorem kappa_lambda_3_RS_eq_zero L164
def kappa_lambda_4_RS L168
theorem kappa_lambda_4_RS_eq_one_third L170
def lambda_6_RS L175
theorem lambda_6_RS_pos L177
structure HiggsCoshBSMFalsifier L195
theorem higgsCoshBSMFalsifier L202
def kinetic_term_shape_frontier L231
theorem kinetic_term_shape_frontier_holds L233