Physics Electroweak Bosons

The weak force carriers

The W and Z bosons are the carriers of the weak nuclear force, the interaction responsible for radioactive beta decay and the fusion reactions that power the Sun. Unlike the massless photon, which carries the electromagnetic force, the W and Z bosons are extremely heavy. The W boson has a measured mass of about 80.37 GeV, and the Z boson is heavier at about 91.19 GeV. Their masses are not arbitrary; in the Standard Model of particle physics, they arise from the Higgs mechanism, in which a field called the Higgs field acquires a nonzero value everywhere in space, breaking the electroweak symmetry and giving mass to these particles.

The relationship between the two masses is set by the weak mixing angle, also called the Weinberg angle θ_W. The theory predicts that m_Z = m_W / cos(θ_W), and the measured masses obey this relation. The sine squared of this angle, sin²θ_W, is measured to be about 0.231. This angle also connects the electromagnetic and weak couplings, describing how the two forces mix. The Higgs field's vacuum expectation value, the constant background value it takes everywhere, is about 246 GeV, which sets the overall scale for the W and Z masses.

In Recognition Science, the framework models the electroweak sector by placing these known quantities on its phi-ladder, a sequence of powers of the golden ratio φ ≈ 1.618. The framework's library, a machine-checked collection of formal theorems, defines the vacuum expectation value at 246.22 GeV and the measured masses as constants. It proves several basic facts about them: the W boson mass is near 80 GeV, the Z boson mass is near 91 GeV, the Z is heavier than the W, and the ratio of the W mass to the Z mass is close to cos(θ_W), within 0.005. It also proves that the ratio of the Higgs boson mass to the W mass is within 0.1 of the golden ratio φ itself, a numerical coincidence the framework highlights.

These are not derivations of the masses from first principles. The framework takes the measured values as definitions and then proves approximate relations among them. The theorem that the W-to-Z mass ratio equals cos(θ_W) is a formal restatement of the Standard Model relation, not a new prediction. The framework's contribution is to show that these numbers sit on its phi-ladder and that some simple ratios among them approximate φ, but it does not explain why the vacuum expectation value takes the value it does. The origin of the electroweak scale remains an open target.

/-- W boson mass in GeV. -/
def wBosonMass_GeV : ℝ := 80.3692

/-- Z boson mass in GeV. -/
def zBosonMass_GeV : ℝ := 91.1876

/-- Predicted W/Z ratio = cos(θW). -/
theorem wz_ratio_equals_cos_theta :
    |wz_mass_ratio - cos_theta_W| < 0.005 := by
  -- wz_mass_ratio = 80.3692 / 91.1876 ≈ 0.88136
  -- cos_theta_W = sqrt(1 - 0.23122) = sqrt(0.76878) ≈ 0.87683
  -- |0.88136 - 0.87683| = 0.00453 < 0.005
  simp only [wz_mass_ratio, wBosonMass_GeV, zBosonMass_GeV, cos_theta_W, sin2_theta_W]
  -- Need: |80.3692/91.1876 - sqrt(0.76878)| < 0.005
  -- Bounds on ratio: 0.8813 < ratio < 0.8814
  have h_ratio_lo : (80.3692 : ℝ) / 91.1876 > 0.8813 := by norm_num
  have h_ratio_hi : (80.3692 : ℝ) / 91.1876 < 0.8814 := by norm_num
  -- Bounds on sqrt: 0.8768 < sqrt(0.76878) < 0.8769
  -- 0.8768^2 = 0.76877824, 0.8769^2 = 0.76895361
  have h_sqrt_lo : sqrt 0.76878 > 0.8768 := by
    have h_sq : (0.8768 : ℝ)^2 < 0.76878 := by norm_num
    exact (Real.lt_sqrt (by norm_num : (0 : ℝ) ≤ 0.8768)).mpr h_sq
  have h_sqrt_hi : sqrt 0.76878 < 0.8769 := by
    have h_sq : 0.76878 < (0.8769 : ℝ)^2 := by norm_num
    have h_pos : (0 : ℝ) ≤ 0.76878 := by norm_num
    have h := Real.sqrt_lt_sqrt h_pos h_sq
    simp only [Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 0.8769)] at h
    exact h
  -- Difference: (0.8813, 0.8814) - (0.8768, 0.8769) = (0.0044, 0.0046)
  rw [abs_lt]
  constructor <;> linarith

/-- Weak mixing angle sin²θW (on-shell scheme). -/
def sin2_theta_W : ℝ := 0.23122

/-- Higgs VEV in GeV. -/
def vev_GeV : ℝ := 246.22

/-- Higgs to W ratio ≈ 1.56 ≈ φ. -/
theorem higgs_w_near_phi : |higgs_w_ratio - phi| < 0.1 := by
  -- 125.25 / 80.3692 ≈ 1.5585, φ ∈ (1.61, 1.62)
  -- |1.5585 - 1.618| ≈ 0.06 < 0.1
  simp only [higgs_w_ratio, higgsMass_GeV, wBosonMass_GeV]
  have hphi_lo : phi > 1.61 := phi_gt_onePointSixOne
  have hphi_hi : phi < 1.62 := phi_lt_onePointSixTwo
  have h1 : (125.25 : ℝ) / 80.3692 > 1.55 := by norm_num
  have h2 : (125.25 : ℝ) / 80.3692 < 1.56 := by norm_num
  rw [abs_lt]
  constructor <;> linarith

What this page does not claim

No derivation of the W and Z masses from the framework's cost function is claimed. No explanation for the value of the weak mixing angle is claimed. No claim that the electroweak scale is uniquely forced by the framework is made.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/ElectroweakBosons.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: