Masses Electroweak Masses Z Mass Bounds

The Z boson bound

The Z boson is one of the heavy carriers of the weak force, with a measured mass of 91187.6 MeV according to the Particle Data Group 2024 listing. In the Recognition Science framework, this mass is not a free parameter. The framework's electroweak sector places the Z at rung 1, a specific position in its internal structure, and derives the mass from the golden ratio: m_Z = 2 × φ^51 / 10^6 MeV. The declaration z_mass_bounds is a machine-checked theorem stating that this predicted value lies strictly between 91075.09 and 91075.10 MeV.

That narrow window matters because it makes the prediction testable. The same theorem file also proves that the predicted mass is within 0.13% of the PDG measured value. The framework's library of formal theorems, a machine-checked collection, verifies both the bound and the relative error. A separate structure, EWCert, bundles these results into a single verification certificate, and the theorem ew_cert_exists proves such a certificate exists.

In Recognition Science, the framework models the W boson mass as derived from the Z via the Weinberg angle: m_W = m_Z × cos(θ_W), where sin²θ_W = (3 − φ)/6. The theorem wz_ratio_eq_cos states that the W/Z mass ratio equals cos(θ_W) by construction. This is a definitional relationship, not an independent prediction.

What z_mass_bounds does not claim is as important as what it proves. It does not prove that the framework's prediction is correct, only that it falls in a specific range and is close to the measured value. The agreement is an empirical check, not a derivation of the measured mass from first principles. The framework does not claim to derive the fine-structure constant α; its expression for α is an identification, not a derived coupling. The exact value of α remains an open target.

/-- 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 ew_cert_exists : Nonempty EWCert :=
  ⟨{ z_in_range := z_mass_bounds
     z_error := z_relative_error
     wz_is_cos := wz_ratio_eq_cos }⟩

What this page does not claim

The theorem does not prove the predicted mass equals the measured mass, only that it falls within a stated range. The framework does not claim to derive the fine-structure constant α; its expression is an identification, not a derived coupling. The W/Z mass ratio being cos(θ_W) is a definitional choice, not an independent prediction.

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: