mZ_sq
plain-language theorem explainer
The definition supplies the tree-level squared Z-boson mass as (g² + g'²)v²/4 for arbitrary real gauge couplings g, g' and electroweak scale v. Standard-model builders and recognition-to-SM bridge authors cite it when converting the RS substrate vev into gauge-boson mass ratios. The declaration is a direct one-line algebraic expression with no lemmas or proof steps.
Claim. The squared Z-boson mass is given by $m_Z^2 = (g^2 + {g'}^2) v^2 / 4$, where $g$ and $g'$ are the SU(2)$_L$ and U(1)$_Y$ gauge couplings and $v$ is the Higgs vacuum expectation value.
background
The ElectroweakMassBridge module formalizes the Standard Model tree-level gauge-boson mass relations conditional on a positive electroweak scale $v$ (imported from HiggsEFTBridge) and arbitrary positive gauge couplings $g, g'$. It encodes the relations $m_W^2 = g^2 v^2 / 4$ and $m_Z^2 = (g^2 + g'^2) v^2 / 4$, which immediately yield the Weinberg-angle identities $m_W / m_Z = g / sqrt(g^2 + g'^2)$ and $sin^2 theta_W = g'^2 / (g^2 + g'^2)$. The module keeps $g$ and $g'$ as free parameters; numerical calibration against the recognition substrate remains a separate open task tracked under OPEN_NORMALIZATION.
proof idea
The declaration is a one-line definition that directly encodes the algebraic expression (g ^ 2 + gp ^ 2) * v ^ 2 / 4. No upstream lemmas are invoked; the body is the explicit formula itself.
why it matters
This definition is the central building block for the ElectroweakMassBridgeCert structure and for all ratio theorems such as mW_over_mZ_sq, mW_over_mZ_eq_cos_thetaW and mW_sq_le_mZ_sq. It completes the gauge-mass portion of the recognition-to-Standard-Model bridge, leaving only the numerical assignment of g and g' as an open normalization step. It sits downstream of the phi-ladder mass formulas but does not itself invoke J-cost, RCL or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.