wBosonMass_GeV
plain-language theorem explainer
The declaration supplies the numerical value of the W boson mass in GeV units as 80.3692. Particle physicists working in the Recognition Science framework cite it when deriving electroweak relations such as the Higgs-to-W ratio or the weak coupling constant from the VEV scale. The definition is a direct constant assignment with no computation or lemmas.
Claim. The W boson mass equals $80.3692$ GeV.
background
In the Electroweak Bosons module the W boson mass sits inside the RS mechanism for electroweak symmetry breaking, where the Higgs field acquires a VEV near 246 GeV that breaks SU(2)_L × U(1)_Y to U(1)_EM and corresponds to a J-cost minimum. The upstream Z definition supplies the integer map for anchor relations: Z(sector, Q) equals (6Q)^2 + (6Q)^4 for leptons and 4 + (6Q)^2 + (6Q)^4 for quarks, used to place masses on the phi-ladder. The module states that the VEV appears at a specific rung on the phi-ladder and that the W/Z mass ratio equals cos(theta_W).
proof idea
The definition is a direct numerical assignment of the constant 80.3692 with no lemmas applied.
why it matters
This constant feeds the parent results higgs_w_near_phi (Higgs-to-W ratio near phi) and weak_coupling_approx (g near 0.653), as well as predicted_z_from_w and vev_determines_scale. It fills the electroweak scale prediction in the RS framework, consistent with the phi-ladder placement and the eight-tick octave structure. It touches the open question of exact derivation from the J-cost minimum rather than external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.