module module

`IndisputableMonolith.Constants.ElectroweakVEVStructure`

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

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

IndisputableMonolith.Constants.FermiConstantScoreCard module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.QFT.ElectroweakScaleStructure module_import

declarations in this module (14)

theorem vev_not_free_parameter L27
def vev_from_ledger L31
theorem vev_structure L36
theorem vev_implies_scale L39
theorem vev_phi_window L43
theorem vev_implies_phi_ne_one L47
theorem vev_phi_ladder_position L66
theorem vev_wz_mass_hierarchy L87
theorem hierarchy_problem_dissolution L108
theorem c020_derivation_strategy L130
def vev_canonical L151
theorem vev_in_range L154
theorem vev_canonical_pos L158
theorem vev_electron_rung_27_order L164