mZ
plain-language theorem explainer
The declaration defines the Z-boson mass as the positive square root of the gauge-coupling expression built from the recognition-substrate vev. Electroweak model builders working inside Recognition Science cite it when they need the explicit m_Z that enters mass-ratio identities. The definition is a one-line wrapper that applies the square-root operation to the upstream squared-mass term.
Claim. $m_Z(g,g',v)=√[(g² + g'²)v²/4]$
background
The Electroweak Mass Bridge module formalizes the tree-level Standard-Model gauge-boson masses from the recognition-substrate scale v together with arbitrary positive couplings g and g'. It records the relations m_W² = g² v²/4 and m_Z² = (g² + g'²)v²/4, together with the identification m_W/m_Z = cos θ_W. The present definition of m_Z rests on the upstream sibling mZ_sq, whose doc-comment states m_Z² = (g² + g'²)v²/4.
proof idea
One-line wrapper that applies Real.sqrt to mZ_sq g gp v.
why it matters
This definition supplies the concrete m_Z term required by the downstream theorem mW_over_mZ_eq_cos_thetaW, which proves the mass ratio equals cos θ_W under positivity. It completes the gauge-mass bridge from the RS vev (imported via HiggsEFTBridge) to the Standard-Model relations, leaving the numerical calibration of g and g' as the remaining open step tracked under OPEN_NORMALIZATION.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.