wMassSq_over_vev
plain-language theorem explainer
The declaration supplies the squared mass of the W boson in terms of the SU(2) gauge coupling g and the Higgs vacuum expectation value v. Particle physicists working on electroweak symmetry breaking would cite this when deriving mass ratios inside the Recognition Science Q3 framework. The definition is a direct algebraic transcription of the covariant derivative term in the Higgs kinetic Lagrangian.
Claim. $m_W^2 = g^2 v^2 / 4$, where $g$ is the SU(2)$_L$ coupling constant and $v$ is the Higgs vacuum expectation value.
background
The module formalizes the representation theory of the quaternion group Q₃ (or Q₈) and its role in the EW symmetry breaking pattern. Q₃ appears in RS as the symmetry group of the 8-tick cycle. Under SU(2)×U(1) → U(1) the Higgs doublet splits into three Goldstone modes eaten by W± and Z plus the physical spin-0 Higgs. The mass ratio m_H / m_W follows from the ratio of Casimir eigenvalues of the spin-0 and spin-1 sectors together with the forced J-cost curvature J″(1) = 1. In the φ-ladder the W boson occupies rung 21; g² is expressed as 4 sin²θ_W · (m_Z / v)² with sin²θ_W = (3 - φ)/6.
proof idea
This is a one-line definition that directly transcribes the standard electroweak formula m_W² = g²v²/4 from the Higgs kinetic term. No lemmas or tactics are invoked; the body is the literal algebraic expression.
why it matters
The definition supplies the W-mass squared input required for the Higgs-to-W ratio inside the Q3 representation module. It anchors the mass formula on the φ-ladder (rung 21 for W) and connects to the eight-tick octave via the quaternion symmetry group. The relation supports the RS derivation of m_H / m_W = 2/g once g is fixed by the Weinberg angle (3 - φ)/6. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.