module module

`IndisputableMonolith.StandardModel.HiggsYukawaBridge`

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

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith module_import
IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit module_import
IndisputableMonolith.StandardModel.HiggsObservableSkeleton module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Masses.MassLaw module_import

declarations in this module (11)

def yukawa_SM L56
theorem yukawa_SM_pos L60
theorem yukawa_SM_phi_scaling L70
theorem yukawa_SM_ratio_adjacent L81
theorem yukawa_SM_ratio_independent_of_v L92
theorem yukawa_SM_phi_pow_scaling L109
def YukawaNormalizationHypothesis L137
theorem yukawa_SM_pos_of_hypothesis L142
structure HiggsYukawaBridgeCert L153
def higgsYukawaBridgeCert L168
theorem higgsYukawaBridgeCert_inhabited L174