wBosonMass
plain-language theorem explainer
The wBosonMass definition supplies the tree-level Higgs mechanism expression for the charged weak boson mass as half the product of the SU(2) coupling and the vacuum expectation value. Particle physicists matching Recognition Science mass predictions to collider data would cite it when placing the W boson on the phi-ladder. It is realized as a direct one-line algebraic assignment with no lemmas or tactics.
Claim. The W boson mass satisfies $m_W = g v / 2$, where $g$ is the SU(2)_L gauge coupling and $v$ is the Higgs vacuum expectation value at the J-cost minimum.
background
The ElectroweakBreaking module identifies the Higgs potential with the J-cost functional whose minimum fixes the vacuum expectation value. Recognition Science operates in RS-native units supplied by the upstream U definition, where the speed of light equals one and lengths are measured in voxels. The anchor map Z from the Masses.Anchor module assigns integer charges to lepton and quark sectors, while the PrimitiveDistinction.from theorem reduces seven axioms to four structural conditions plus three definitional facts that keep the ledger collision-free.
proof idea
The declaration is a one-line definition that directly transcribes the standard tree-level formula m_W = g v / 2. No lemmas are applied and no tactics are used; the body is the literal arithmetic expression.
why it matters
This definition is invoked by the wBosonMass declaration in the QFT.HiggsMechanism module, which completes the electroweak mass spectrum. It fills the SM-009 target of deriving spontaneous symmetry breaking SU(2)_L × U(1)_Y → U(1)_EM from the J-cost minimum rather than an ad-hoc potential, thereby anchoring the observed W mass to the phi-ladder once g and v are fixed by the anchor relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.