Physics Wboson Absolute Score Card

The W boson scorecard

The W boson is one of the heavy particles that carry the weak nuclear force, the interaction behind radioactive decay. Its mass, about 80.4 GeV, is a standard measurement in particle physics. The scorecard, a discrete record of derived claims with their proofs, in the Recognition Science framework starts from the Z boson mass, the weak mixing angle, and the known relation between the two masses, and produces a prediction for the W mass.

The derivation uses three ingredients, each itself derived within the framework rather than chosen to fit data. The Z boson mass comes from a phi-ladder rung, a step in a sequence of masses spaced by powers of the golden ratio. The weak mixing angle, the parameter that describes how the Z and W masses differ, is fixed by the framework's gauge embedding geometry. The relation between the masses is the standard one from the electroweak theory: m_W equals m_Z times the cosine of the weak mixing angle.

The framework proves, in its machine-checked library of formal theorems, that the square of the cosine of the mixing angle equals (3 + phi) / 6, where phi is the golden ratio. It also proves this value lies between 0.769 and 0.771. From this, the predicted W mass falls in the band from 79.921 to 79.922 GeV. The measured value from the Particle Data Group 2024 is 80.3692 GeV, with an uncertainty of 0.0133 GeV. The residual difference is about 0.56 percent, which the framework attributes to radiative corrections from the running of the fine-structure constant.

The scorecard certifies six claims together: the closed form for the cosine squared, the numerical band for it, the corresponding band for the sine squared, the mass ratio relation, the count of exactly three inputs, and the statement that zero parameters are fitted. The certificate is a single theorem that packages all six. The framework's library checks the certificate with no gaps and no extra assumptions beyond the standard logical axioms.

What this establishes in plain language is a test of the framework's internal consistency. The framework does not tune its parameters to match the W mass; it derives the ingredients from its own structure and then compares. The comparison against the measured value is a check on the framework's predictions, not a proof that the framework is correct. The 0.56 percent gap is a real discrepancy that the framework explains by radiative corrections, but that explanation is itself a further calculation, not part of the scorecard's formal proof.

/-- cos²θ_W = (3+φ)/6 from the RS Weinberg angle. -/
theorem cos2_theta_W_closed_form :
    cos2_theta_W_rs = (3 + phi) / 6 := by
  unfold cos2_theta_W_rs sin2_theta_W_rs
  ring

/-- cos²θ_W > 0.769. Since φ > 1.61, we get (3+φ)/6 > 4.61/6 > 0.768. -/
theorem cos2_gt : (0.769 : ℝ) < cos2_theta_W_rs := by
  rw [cos2_theta_W_closed_form]
  have hphi : (1.614 : ℝ) < phi := by
    unfold phi
    have h5 : (2.228 : ℝ) < Real.sqrt 5 := by
      rw [show (2.228 : ℝ) = Real.sqrt (2.228 ^ 2) from by
        rw [Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2.228)]]
      exact Real.sqrt_lt_sqrt (by positivity) (by norm_num)
    linarith
  linarith

/-- cos²θ_W < 0.771. Since φ < 1.62, we get (3+φ)/6 < 4.62/6 < 0.770. -/
theorem cos2_lt : cos2_theta_W_rs < (0.771 : ℝ) := by
  rw [cos2_theta_W_closed_form]
  have hphi : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
  linarith

/-- The W/Z mass ratio is cos θ_W, which is √((3+φ)/6). -/
theorem wz_ratio_is_cos_theta : w_pred / z_pred = cos_theta_W_rs :=
  wz_ratio_eq_cos

theorem zero_free_params : free_params_w_mass = 0 := rfl

theorem wBosonAbsoluteScoreCardCert_holds :
    Nonempty WBosonAbsoluteScoreCardCert :=
  ⟨{ cos2_closed := cos2_theta_W_closed_form
     cos2_band := ⟨cos2_gt, cos2_lt⟩
     sin2_band := ⟨sin2_gt, sin2_lt⟩
     wz_is_cos := wz_ratio_is_cos_theta
     input_count := three_inputs
     zero_free := zero_free_params }⟩

What this page does not claim

The measured W mass is not derived by the framework; the comparison against PDG 2024 is an empirical check. The 0.56 percent residual is not formally shown to be fully explained by radiative corrections. The framework does not prove the standard electroweak relation between m_W and m_Z; it assumes it as an input.

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/WBosonAbsoluteScoreCard.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: