Masses Electroweak Masses Wz Ratio Eq Cos

The W/Z ratio relation

In the standard model of particle physics, the masses of the W and Z bosons are not independent: the W is lighter, and the ratio of their masses equals the cosine of the Weinberg angle, the parameter that measures how much the electroweak force mixes its two underlying symmetries. The Recognition Science (RS) framework encodes the same relationship in its own vocabulary. Its declaration wz_ratio_eq_cos states that, within the framework's mass model, the predicted W mass divided by the predicted Z mass equals the cosine of the framework's Weinberg angle.

This is a theorem in the machine-checked library of formal theorems, meaning it is proved from definitions by a computer-verified proof. The proof itself is trivial once the definitions are fixed: the W prediction is defined as the Z prediction multiplied by the cosine, so dividing by the Z prediction cancels to give the cosine. The declaration does not derive the Weinberg angle from first principles. It takes the angle as a defined quantity, with sin²θ_W = (3 − φ)/6, where φ is the golden ratio. The theorem's content is the algebraic identity, not the physical origin of the angle.

The framework's library also proves bounds on the Z mass prediction: it lies between 91075.09 and 91075.10 MeV, which is within 0.13% of the PDG 2024 experimental value of 91187.6 MeV. The W mass prediction inherits the Z prediction through the cosine relation. These numerical agreements are empirical checks, not theorems. The identity w_pred / z_pred = cos_theta_W_rs is exact by construction, while the comparison to measured particle masses is a separate, empirical claim.

In plain terms, the declaration says: if you accept the framework's definitions for the Z mass and the Weinberg angle, then the W mass is forced to be the Z mass times the cosine of that angle. It does not say the framework predicts the Weinberg angle from nothing, nor that the framework's mass values match experiment to any particular precision. Those are separate claims, with separate evidence.

/-- 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

/-- 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

/-- 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]

What this page does not claim

The declaration does not derive the Weinberg angle from first principles; it takes it as a defined quantity. The declaration does not assert that the framework's mass predictions match experiment to any particular precision. The declaration does not claim that the W/Z ratio is measured to be exactly cos(θ_W) in nature; it only states the identity within the framework's definitions.

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: