zBosonMass
plain-language theorem explainer
The zBosonMass definition supplies the Z boson mass as m_Z = v √(g² + g'²)/2 expressed through the Higgs vacuum expectation value v and the SU(2) and U(1) couplings. Particle physicists working inside the Recognition Science derivation of the Standard Model would cite this when connecting J-cost minima to electroweak masses. The implementation is a direct noncomputable definition that transcribes the conventional Higgs mechanism formula with no auxiliary lemmas.
Claim. $m_Z = v √(g² + g'²)/2$, where $v$ is the Higgs vacuum expectation value, $g$ the SU(2)_L gauge coupling, and $g'$ the U(1)_Y hypercharge coupling.
background
The Electroweak Symmetry Breaking module reinterprets the Standard Model Higgs mechanism through Recognition Science: the Higgs potential equals the J-cost functional, the vacuum expectation value v equals the J-cost minimum, and spontaneous symmetry breaking SU(2)_L × U(1)_Y → U(1)_EM follows when the Higgs field selects that minimum. The module states that W and Z bosons acquire mass while the photon remains massless once v is fixed. Upstream anchors from the Masses module calibrate the integer ladder used for mass formulas, and the PhiForcing import enforces consistency with the self-similar fixed point.
proof idea
The declaration is a one-line definition that directly transcribes the textbook Higgs mechanism mass formula for the Z boson using arithmetic and square root on the parameters g, g', and v. No lemmas or tactics are invoked beyond the algebraic expression itself.
why it matters
This definition supplies the Z mass expression consumed by the HiggsMechanism module to relate m_Z to m_W through the Weinberg angle. It completes the SM-009 target of deriving electroweak masses from J-cost minimization inside the Recognition Science chain. The placement connects to the eight-tick octave and D = 3 through the underlying forcing structure while leaving open the derivation of the numerical value of v from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.