def definition def or abbrev

`mW`

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

formal statement (Lean)

  56def mW (g v : ℝ) : ℝ := Real.sqrt (mW_sq g v)

Definition body.

  57
  58/-- Z boson mass: `m_Z = √(g² + g'²) · v / 2` (for `g, g', v > 0`). -/

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

gf_from_mw in IndisputableMonolith.Physics.WeakForceEmergence decl_use
gf_matches in IndisputableMonolith.Physics.WeakForceEmergence decl_use
mW_over_mZ_eq_cos_thetaW in IndisputableMonolith.StandardModel.ElectroweakMassBridge decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
mW_sq in IndisputableMonolith.StandardModel.ElectroweakMassBridge decl_use
m_Z in IndisputableMonolith.StandardModel.WZMassRatio decl_use