mW
plain-language theorem explainer
Defines the W boson mass as half the product of the SU(2) gauge coupling g and the vacuum expectation value v. Researchers deriving electroweak parameters from the recognition substrate would reference this when computing the Fermi constant or checking mass ratios. The implementation is a direct square-root wrapper around the squared-mass definition mW_sq.
Claim. $m_W(g, v) := g v / 2$ for $g, v > 0$, obtained by taking the positive square root of $g^2 v^2 / 4$.
background
The Electroweak Mass Bridge module derives the Standard Model gauge-boson mass relations from the recognition-substrate scale v together with positive gauge couplings g and g'. It states the relations m_W² = g² v² / 4 and m_Z² = (g² + g'²) v² / 4, along with the Weinberg angle identities. The definition of mW relies on the sibling definition mW_sq, which encodes the squared mass directly as g² v² / 4. Upstream, the anchor Z from Masses.Anchor provides the integer map for sector charges, while the forcing structure in UniversalForcingSelfReference supplies the meta-realization context, though the mass bridge operates independently on the positive reals.
proof idea
This is a one-line definition that applies Real.sqrt to the output of mW_sq g v. No lemmas are invoked beyond the built-in square-root function on reals; the positivity of the argument is guaranteed by the upstream mW_sq definition and the positivity hypotheses in calling theorems.
why it matters
It is used in WeakForceEmergence to define gf_from_mw and to prove gf_matches, which verifies the Fermi constant numerically within 10%. It also underpins the theorem mW_over_mZ_eq_cos_thetaW establishing the cosine relation. This places the electroweak masses on the same v from HiggsEFTBridge, advancing the bridge between recognition forcing chain and Standard Model phenomenology while leaving the calibration of g and g' as an open step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.