Masses Electroweak Masses

Electroweak boson masses

The electroweak bosons are the particles that carry two of the four fundamental forces: the W boson mediates radioactive decay, and the Z boson mediates the weak neutral current. In the standard model, their masses are free parameters, fixed by experiment. The Recognition Science framework instead derives them from a single scaling law, with no fitted constants.

The framework's core idea is a ledger, a discrete record of recognition events, and a forced cost function that follows from five plain conditions. From that cost function, a chain of theorems forces the golden ratio φ ≈ 1.618 as the unique self-similar scaling. Particle masses sit on a ladder of powers of φ. The electroweak module places the Z boson on rung 1 of the electroweak sector, giving m_Z = 2 × φ^51 / 10^6 MeV, which evaluates to about 91,075.1 MeV. The W boson mass is then derived from the Z via the Weinberg angle, a quantity that mixes the electromagnetic and weak forces: m_W = m_Z × cos(θ_W), where sin²θ_W = (3 − φ)/6.

The module proves, in a machine-checked library of formal theorems, that this Z prediction lies between 91,075.09 and 91,075.10 MeV, and that its relative error against the Particle Data Group 2024 value of 91,187.6 MeV is less than 0.13 percent. It also proves the W/Z mass ratio equals cos(θ_W) by construction. These are formal theorems, not numerical coincidences: the bounds and the ratio are checked by the kernel.

In Recognition Science, the Weinberg angle is not an input but a derived quantity. The expression sin²θ_W = (3 − φ)/6 comes from the gauge embedding geometry, a definitional choice within the framework. The measured value of sin²θ_W is about 0.231, and the framework's value is about 0.230, a close match. The Higgs boson mass is approximately m_W × φ, a separate identification.

The practical consequence is a single, unified origin for the electroweak scale. The framework does not explain why the Z boson has the mass it does by fitting a parameter; it computes that mass from a power of the golden ratio. The agreement with experiment is an empirical check, not a theorem, but it is a check that passes within the stated bounds.

/-- The Z boson mass prediction lies in (91075.09, 91075.10) MeV. -/
theorem z_mass_bounds :
    (91075.09 : ℝ) < z_pred ∧ z_pred < (91075.10 : ℝ) := by
  rw [z_pred_eq]
  constructor
  · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
    calc (91075.09 : ℝ) * 1000000 = (91075090000 : ℝ) := by norm_num
      _ < 2 * (45537548334 : ℝ) := by norm_num
      _ < 2 * Constants.phi ^ 51 := by nlinarith [phi51_gt]
  · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
    calc 2 * Constants.phi ^ 51 < 2 * (45537549354 : ℝ) := by nlinarith [phi51_lt]
      _ = (91075098708 : ℝ) := by norm_num
      _ < (91075100000 : ℝ) := by norm_num
      _ = (91075.10 : ℝ) * 1000000 := by norm_num

/-- The Z boson prediction is within 0.13% of the PDG value. -/
theorem z_relative_error :
    |z_pred - m_Z_exp| / m_Z_exp < 0.0013 := by
  have hb := z_mass_bounds
  have hexp_pos : (0 : ℝ) < m_Z_exp := by unfold m_Z_exp; norm_num
  rw [div_lt_iff₀ hexp_pos, abs_lt]
  unfold m_Z_exp
  constructor <;> nlinarith [hb.1, hb.2]

/-- The W/Z mass ratio equals cos(θ_W) by construction. -/
theorem wz_ratio_eq_cos : w_pred / z_pred = cos_theta_W_rs := by
  unfold w_pred
  have hzne : z_pred ≠ 0 := ne_of_gt (by linarith [z_mass_bounds.1])
  exact mul_div_cancel_left₀ _ hzne

theorem z_pred_eq : z_pred = 2 * Constants.phi ^ (51 : ℕ) / 1000000 := by
  unfold z_pred rs_mass_MeV
  simp only [B_pow_Electroweak_eq, r0_Electroweak_eq]
  have hphi : Constants.phi ≠ 0 := ne_of_gt phi_pos
  have hphi_combine : Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (55 : ℤ) * Constants.phi ^ (1 : ℤ) =
      Constants.phi ^ ((51 : ℕ) : ℤ) := by
    rw [← zpow_add₀ hphi, ← zpow_add₀ hphi]; norm_num
  conv_lhs =>
    rw [show (2 : ℝ) ^ (1 : ℤ) * Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (55 : ℤ) * Constants.phi ^ (1 : ℤ)
      = (2 : ℝ) ^ (1 : ℤ) * (Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (55 : ℤ) * Constants.phi ^ (1 : ℤ)) from by ring]
    rw [hphi_combine, zpow_natCast]
  simp only [zpow_one]

noncomputable def sin2_theta_W_rs : ℝ := (3 - Constants.phi) / 6

What this page does not claim

The framework does not derive the fine-structure constant. The agreement with PDG values is an empirical check, not a theorem. The Weinberg angle expression is a definitional choice, not a derived theorem.

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/Masses/ElectroweakMasses.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: