mW_sq
plain-language theorem explainer
The definition supplies the squared W-boson mass as g squared times v squared over four, with g the SU(2) gauge coupling and v the electroweak scale taken from the recognition substrate. Researchers bridging Recognition Science to the Standard Model cite it when stating tree-level gauge masses conditional on positive couplings. The declaration is a direct one-line abbreviation matching the textbook formula with no additional lemmas or hypotheses.
Claim. The squared mass of the W boson satisfies $m_W^2 = g^2 v^2 / 4$, where $g$ is the weak isospin gauge coupling and $v$ is the vacuum expectation value supplied by the recognition-substrate Higgs scale.
background
This module derives the Standard-Model gauge-boson mass relations from the recognition-substrate scale $v$ together with arbitrary positive gauge couplings $g, g'$. The electroweak scale $v$ is imported from HiggsEFTBridge; the module treats $g$ and $g'$ as free positive reals whose numerical values remain an empirical input. Upstream anchor maps Z supply the integer sector labels used for particle-mass anchoring elsewhere in the framework, though the present definition does not invoke them.
proof idea
The declaration is a direct definition whose body is the algebraic expression $g^2 * v^2 / 4$. No lemmas or tactics are applied; the line simply encodes the standard tree-level formula.
why it matters
This definition supplies the base expression for the entire suite of W/Z relations in the module, including the master certificate ElectroweakMassBridgeCert and the ratio theorems mW_over_mZ_sq and mW_over_mZ_eq_cos_thetaW. It realizes the gauge-mass bridge step that lets the SM tree-level relations hold unconditionally once $v$ is taken from the RS substrate. The open normalization task of fixing $g, g'$ numerically from the phi-ladder lies outside this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.