def definition def or abbrev

`m_W`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  47noncomputable def m_W : ℝ := 80.377

proof body

Definition body.

  48
  49/-- Z boson mass (GeV). -/

used by (35)

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

hierarchy_problem_dissolution in IndisputableMonolith.Constants.ElectroweakVEVStructure decl_use
vev_phi_ladder_position in IndisputableMonolith.Constants.ElectroweakVEVStructure decl_use
vev_wz_mass_hierarchy in IndisputableMonolith.Constants.ElectroweakVEVStructure decl_use
w_mass_atlas_measurement in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_cdf_measurement in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_from_z in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_phi_ladder_position in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_rs_prediction in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_sigma_comparison in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_sm_prediction in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_z_mass_ratio in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
z_relative_error in IndisputableMonolith.Masses.ElectroweakMasses decl_use
dmMassRatio_eq in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
gap45_eq in IndisputableMonolith.Physics.DarkMatterMassFromGap45 decl_use
predicted_z_from_w in IndisputableMonolith.Physics.ElectroweakBosons decl_use
GaugeBosonMass in IndisputableMonolith.QFT.HiggsMechanism decl_use
wBosonMass in IndisputableMonolith.QFT.HiggsMechanism decl_use
higgsMass_observed in IndisputableMonolith.StandardModel.ElectroweakBreaking decl_use
wZRatio in IndisputableMonolith.StandardModel.ElectroweakBreaking decl_use
zBosonMass in IndisputableMonolith.StandardModel.ElectroweakBreaking decl_use
mZ_sq in IndisputableMonolith.StandardModel.ElectroweakMassBridge decl_use
mH_prediction_in_interval in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
higgsMassRatio in IndisputableMonolith.StandardModel.Q3Representations decl_use
higgs_rung_prediction in IndisputableMonolith.StandardModel.Q3Representations decl_use
wMassSq_over_vev in IndisputableMonolith.StandardModel.Q3Representations decl_use
w_rung in IndisputableMonolith.StandardModel.Q3Representations decl_use
runningAngle in IndisputableMonolith.StandardModel.WeinbergAngle decl_use
bestPhiPrediction in IndisputableMonolith.StandardModel.WZMassRatio decl_use
experimentalStatus in IndisputableMonolith.StandardModel.WZMassRatio decl_use
implications in IndisputableMonolith.StandardModel.WZMassRatio decl_use

… and 5 more

depends on (2)

Lean names referenced from this declaration's body.

Z in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use