module module

`IndisputableMonolith.Cosmology.WMassAnomalyStructure`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.QFT.ElectroweakScaleStructure module_import

declarations in this module (15)

theorem has_ew_scale_structure L83
def w_mass_anomaly_from_ledger L87
theorem w_mass_anomaly_structure L89
theorem w_mass_implies_ew_scale L92
theorem w_mass_phi_ladder_position L102
theorem w_mass_rs_prediction L120
theorem w_mass_sm_prediction L134
theorem w_mass_cdf_measurement L141
theorem w_mass_atlas_measurement L148
theorem w_z_mass_ratio L162
theorem w_mass_from_z L176
theorem w_mass_anomaly_explained L194
theorem w_mass_sigma_comparison L211
structure WMassAnomalyResolution L250
theorem w_mass_anomaly_resolved L262